equal
deleted
inserted
replaced
19 |
19 |
20 mkdir -p "$ISABELLE_TMP_PREFIX" || exit $? |
20 mkdir -p "$ISABELLE_TMP_PREFIX" || exit $? |
21 |
21 |
22 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null |
22 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null |
23 then |
23 then |
24 exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" |
24 exec "$ISABELLE_LINE_EDITOR" isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" |
25 else |
25 else |
26 echo "### No line editor: \"$ISABELLE_LINE_EDITOR\"" |
26 echo "### No line editor: \"$ISABELLE_LINE_EDITOR\"" |
27 exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" |
27 exec isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" |
28 fi |
28 fi |