VandeVondele Joost Tue, 16 Sep 2014 02:31:36 -0700
> Does the following patch fix this? Works for me with dejagnu 1.5.1. and works for me with 1.4.4
Joost