# HG changeset patch
# User wenzelm
# Date 1578910764 -3600
# Node ID 201486ced92d0fd9685338ade9f36d97f4dedb2f
# Parent  85274743f789818f644abf3ec75748e04d672a6e
clarified output channel;

diff -r 85274743f789 -r 201486ced92d lib/Tools/client
--- 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
diff -r 85274743f789 -r 201486ced92d lib/Tools/console
--- 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
diff -r 85274743f789 -r 201486ced92d lib/browser/build
--- 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