Re: dejagnu 1.5

[Mike Stump]

Ah, I found it…  It was a local config that hid unknown.  :-(  Sorry for the 
noise.

_______________________________________________
DejaGnu mailing list
DejaGnu@gnu.org
https://lists.gnu.org/mailman/listinfo/dejagnu