# HG changeset patch
# User wenzelm
# Date 1610313431 -3600
# Node ID b15fe413b4d247066fe454dbdd33a318649782d7
# Parent  1105c42722dcbfac3b7feb0472675eb34c80bcf3
tuned message;

diff -r 1105c42722dc -r b15fe413b4d2 src/Doc/JEdit/JEdit.thy
--- 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>}
 
diff -r 1105c42722dc -r b15fe413b4d2 src/Tools/jEdit/lib/Tools/jedit_client
--- 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