> There is decent documentation of the dg-* directives in comments at > the top of $prefix/share/dejagnu/dg.exp, where $prefix refers to your > dejagnu installation. I do agree with Joseph that this ought to be in > the dejagnu manual. The DejaGnu manual needs a lot of work (which I intend to tackle in ernest once I complete my study at the end of June). Ben