--- a/src/Doc/JEdit/JEdit.thy Mon Jan 29 11:18:26 2018 +0100
+++ b/src/Doc/JEdit/JEdit.thy Mon Jan 29 19:26:14 2018 +0100
@@ -236,7 +236,7 @@
(default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)
-P use parent session image
-R open ROOT entry of logic session
- -S NAME edit specified logic session, same as -B -F -R -l NAME
+ -S NAME edit specified logic session, abbreviates -B -F -R -l NAME
-b build only
-d DIR include session directory
-f fresh build
--- a/src/Tools/jEdit/lib/Tools/jedit Mon Jan 29 11:18:26 2018 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Mon Jan 29 19:26:14 2018 +0100
@@ -105,7 +105,7 @@
echo " (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
echo " -P use parent session image"
echo " -R open ROOT entry of logic session"
- echo " -S NAME edit specified logic session, same as abbreviates -B -F -R -l NAME"
+ echo " -S NAME edit specified logic session, abbreviates -B -F -R -l NAME"
echo " -b build only"
echo " -d DIR include session directory"
echo " -f fresh build"