# HG changeset patch
# User wenzelm
# Date 1517250374 -3600
# Node ID a23c3ec2ff28500c0f81d5f759e096c1c84965c1
# Parent  ed9bc7c2d8de695e05d89234c4f8c64a0f26cd4e
more uniform documentation;

diff -r ed9bc7c2d8de -r a23c3ec2ff28 src/Doc/JEdit/JEdit.thy
--- 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
diff -r ed9bc7c2d8de -r a23c3ec2ff28 src/Tools/jEdit/lib/Tools/jedit
--- 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"