lib/Tools/tty
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
 }