tuned message;
authorwenzelm
Sun, 10 Jan 2021 22:17:11 +0100
changeset 73128 b15fe413b4d2
parent 73126 1105c42722dc
child 73129 ff9cd62d2d20
tuned message;
src/Doc/JEdit/JEdit.thy
src/Tools/jEdit/lib/Tools/jedit_client
--- a/src/Doc/JEdit/JEdit.thy	Sun Jan 10 15:48:15 2021 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sun Jan 10 22:17:11 2021 +0100
@@ -296,7 +296,7 @@
   Options are:
     -c           only check presence of server
     -n           only report server name
-    -s NAME      server name (default Isabelle)
+    -s NAME      server name (default "Isabelle")
 
   Connect to already running Isabelle/jEdit instance and open FILES\<close>}
 
--- a/src/Tools/jEdit/lib/Tools/jedit_client	Sun Jan 10 15:48:15 2021 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit_client	Sun Jan 10 22:17:11 2021 +0100
@@ -23,7 +23,7 @@
   echo "  Options are:"
   echo "    -c           only check presence of server"
   echo "    -n           only report server name"
-  echo "    -s NAME      server name (default $SERVER_NAME)"
+  echo "    -s NAME      server name (default \"$SERVER_NAME\")"
   echo
   echo "  Connect to already running Isabelle/jEdit instance and open FILES"
   echo