changeset 48572 | af0f5560ac94 |
parent 29143 | 72c960b2b83e |
child 52062 | 4f91262e7f33 |
--- a/lib/Tools/tty Sat Jul 28 07:26:37 2012 +0200 +++ b/lib/Tools/tty Sat Jul 28 12:59:53 2012 +0200 @@ -17,7 +17,7 @@ echo " -p NAME line editor program name" echo " (default ISABELLE_LINE_EDITOR=\"$ISABELLE_LINE_EDITOR\")" echo - echo " Run Isabelle process with plain tty interaction, and optional line editor." + echo " Run Isabelle process with plain tty interaction and line editor." echo exit 1 }