| changeset 67811 | 33199d033505 |
| parent 67810 | 8ebae6708590 |
| child 67876 | cc4832285c38 |
--- 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