--- a/lib/Tools/client Mon Jan 13 11:18:31 2020 +0100
+++ b/lib/Tools/client Mon Jan 13 11:19:24 2020 +0100
@@ -64,6 +64,6 @@
then
exec "$ISABELLE_LINE_EDITOR" isabelle server "${SERVER_OPTS[@]}"
else
- echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
+ echo >&2 "### No line editor: \"$ISABELLE_LINE_EDITOR\""
exec isabelle server "${SERVER_OPTS[@]}"
fi
--- 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
--- a/lib/browser/build Mon Jan 13 11:18:31 2020 +0100
+++ b/lib/browser/build Mon Jan 13 11:19:24 2020 +0100
@@ -59,7 +59,7 @@
if [ "$OUTDATED" = true ]
then
- echo "### Building graph browser ..."
+ echo >&2 "### Building graph browser ..."
rm -rf classes && mkdir classes