# HG changeset patch
# User wenzelm
# Date 1584139818 -3600
# Node ID e32255318cb290ae9fed6783d25620fc20f50d3d
# Parent  d350aabace23953cc9dda9b644c1a2c432ba926d
proper usage (amending 8c7706b053c7);

diff -r d350aabace23 -r e32255318cb2 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)"