Subject: bug#33821: dejagnu command should list available commands

From: Ben Elliston <[email-masked]>
Date: Sat, 22 Dec 2018 00:09:30 +1100

At present, 'dejagnu' with no arguments gives:

ERROR: no command given

It would be good if it listed the available commands.