proper usage (amending 8c7706b053c7);
authorwenzelm
Fri, 13 Mar 2020 23:50:18 +0100
changeset 71762 e32255318cb2
parent 71761 d350aabace23
child 71763 319599ba28cf
proper usage (amending 8c7706b053c7);
src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Mar 13 23:25:34 2020 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Mar 13 23:50:18 2020 +0100
@@ -100,7 +100,7 @@
   echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
   echo
   echo "  Options are:"
-  echo "    -A NAME      ancestor session for options -R (default: parent)"
+  echo "    -A NAME      ancestor session for option -R (default: parent)"
   echo "    -D NAME=X    set JVM system property"
   echo "    -J OPTION    add JVM runtime option"
   echo "                 (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"