--- 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