At present, 'dejagnu' with no arguments gives: ERROR: no command given
It would be good if it listed the available commands. _______________________________________________ Bug-dejagnu mailing list [email protected] https://lists.gnu.org/mailman/listinfo/bug-dejagnu
