diff -r 8ebae6708590 -r 33199d033505 lib/Tools/client
--- a/lib/Tools/client	Sat Mar 10 13:54:55 2018 +0100
+++ b/lib/Tools/client	Sat Mar 10 14:11:58 2018 +0100
@@ -62,8 +62,8 @@
 
 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
 then
-  exec "$ISABELLE_LINE_EDITOR" isabelle server -C "${SERVER_OPTS[@]}"
+  exec "$ISABELLE_LINE_EDITOR" isabelle server -s -C "${SERVER_OPTS[@]}"
 else
   echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
-  exec isabelle server -C "${SERVER_OPTS[@]}"
+  exec isabelle server -s -C "${SERVER_OPTS[@]}"
 fi