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