lib/Tools/client
changeset 67904 465f43a9f780
parent 67876 cc4832285c38
child 71373 201486ced92d
--- a/lib/Tools/client	Mon Mar 19 18:13:37 2018 +0100
+++ b/lib/Tools/client	Mon Mar 19 19:24:45 2018 +0100
@@ -2,7 +2,7 @@
 #
 # Author: Makarius
 #
-# DESCRIPTION: console interaction for Isabelle server (with line-editor)
+# DESCRIPTION: console interaction for Isabelle servers (with line-editor)
 
 PRG="$(basename "$0")"
 
@@ -15,7 +15,7 @@
   echo "    -n NAME      explicit server name"
   echo "    -p PORT      explicit server port"
   echo
-  echo "  Console interaction for Isabelle server (with line-editor)."
+  echo "  Console interaction for Isabelle servers (with line-editor)."
   echo
   exit 1
 }