equal
deleted
inserted
replaced
12 |
12 |
13 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null |
13 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null |
14 then |
14 then |
15 exec "$ISABELLE_LINE_EDITOR" isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" |
15 exec "$ISABELLE_LINE_EDITOR" isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" |
16 else |
16 else |
17 echo "### No line editor: \"$ISABELLE_LINE_EDITOR\"" |
17 echo >&2 "### No line editor: \"$ISABELLE_LINE_EDITOR\"" |
18 exec isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" |
18 exec isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" |
19 fi |
19 fi |