bug#47533: bug in dejagnu 1.6.3-rc2

[Tom Tromey]

>> Usage: dejagnu <command> [--help|options...]

Jacob> So how should that be written in GNU convention?
Jacob> "dejagnu COMMAND [ --help | OPTIONS... ]"?

Yeah.

Jacob> Is there a description of these conventions somewhere that I have
Jacob> missed or overlooked?

I think it's a convention based on the commenting convention:

https://www.gnu.org/prep/standards/html_node/Comments.html#Comments

>> Third, the use of tabs in the output makes it a bit weird to quote.

Jacob> This was done for convenience, including that the help texts are
Jacob> actually read from the script files where they are "inset" using tabs.  
Jacob> (The line "# ##help" in the dejagnu launcher script introduces its own
Jacob> help text.)  What problems does this cause?

None, it just looks unusual and then when I pasted it into the email, it
indented very weirdly as well.

Tom