| changeset 71373 | 201486ced92d |
| parent 66906 | 03a96b8c7c06 |
| child 74017 | b4e6b82fdb9e |
--- a/lib/Tools/console Mon Jan 13 11:18:31 2020 +0100 +++ b/lib/Tools/console Mon Jan 13 11:19:24 2020 +0100 @@ -14,6 +14,6 @@ then exec "$ISABELLE_LINE_EDITOR" isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" else - echo "### No line editor: \"$ISABELLE_LINE_EDITOR\"" + echo >&2 "### No line editor: \"$ISABELLE_LINE_EDITOR\"" exec isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@" fi