equal
deleted
inserted
replaced
62 |
62 |
63 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null |
63 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null |
64 then |
64 then |
65 exec "$ISABELLE_LINE_EDITOR" isabelle server "${SERVER_OPTS[@]}" |
65 exec "$ISABELLE_LINE_EDITOR" isabelle server "${SERVER_OPTS[@]}" |
66 else |
66 else |
67 echo "### No line editor: \"$ISABELLE_LINE_EDITOR\"" |
67 echo >&2 "### No line editor: \"$ISABELLE_LINE_EDITOR\"" |
68 exec isabelle server "${SERVER_OPTS[@]}" |
68 exec isabelle server "${SERVER_OPTS[@]}" |
69 fi |
69 fi |