diff -r d68b74435605 -r af0f5560ac94 lib/Tools/tty
--- 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
 }