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