Subject: will handle #36293

From: Jacob Bachmeyer <[email-masked]>
Date: Wed, 19 Jun 2019 17:10:35 -0500

package dejagnu
owner 36293 !
thanks

I am already working on related documentation issues that include moving 
the "Adding a new board" section to another chapter.  Fixing this bug is 
now on my local TODO list as part of those efforts.  Rolling this into 
the ongoing work will avoid a merge conflict later.

-- Jacob