# HG changeset patch
# User wenzelm
# Date 1521205987 -3600
# Node ID cc4832285c3875aacbcf05fd929a8a9efb87bded
# Parent  641315ebed02a771b6e8a982bad63718a2095b5f
proper options;

diff -r 641315ebed02 -r cc4832285c38 lib/Tools/client
--- a/lib/Tools/client	Fri Mar 16 14:08:53 2018 +0100
+++ b/lib/Tools/client	Fri Mar 16 14:13:07 2018 +0100
@@ -31,7 +31,7 @@
 
 # options
 
-declare -a SERVER_OPTS=()
+declare -a SERVER_OPTS=(-s -c)
 
 while getopts "n:p:" OPT
 do
@@ -62,8 +62,8 @@
 
 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
 then
-  exec "$ISABELLE_LINE_EDITOR" isabelle server -s -C "${SERVER_OPTS[@]}"
+  exec "$ISABELLE_LINE_EDITOR" isabelle server "${SERVER_OPTS[@]}"
 else
   echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
-  exec isabelle server -s -C "${SERVER_OPTS[@]}"
+  exec isabelle server "${SERVER_OPTS[@]}"
 fi
diff -r 641315ebed02 -r cc4832285c38 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Mar 16 14:08:53 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 16 14:13:07 2018 +0100
@@ -439,7 +439,7 @@
           "n:" -> (arg => name = arg),
           "p:" -> (arg => port = Value.Int.parse(arg)),
           "s" -> (_ => existing_server = true),
-          "X" -> (_ => operation_exit = true))
+          "x" -> (_ => operation_exit = true))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()