On Jul 10, 2017, at 2:21 PM, Mike Stump <mikest...@comcast.net> wrote: > > Someone with such a system will have to drill down into why.
Found it, fixed in dejagnu 1.5.3, just use a newer dejagnu, 1.5.3 or later should be fine. Apparently, I should have just checked it _first_. I didn't expect the fix to lie there.