Rename plaintext documentation from doc/*.doc to doc/*.txt, to avoid
the chronic problem of web sites thinking they're in MS-Word format.
Sigh.  As if Microsoft somehow had a monopoly on the word "document".

Allow MENU EXIT to "exit" to an arbitrary menu.  This is really just a
variant of "MENU GOTO", but it allows displaying an exit marker.