--- 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)"