# HG changeset patch
# User wenzelm
# Date 855249741 -3600
# Node ID b472d703fa06062d0c66ed2a74982e7f03385441
# Parent  ac51a89627ed27751abeb088a065218460861ca7
improved usage msg;

diff -r ac51a89627ed -r b472d703fa06 lib/Tools/expandshort
--- a/lib/Tools/expandshort	Thu Feb 06 17:52:40 1997 +0100
+++ b/lib/Tools/expandshort	Thu Feb 06 18:22:21 1997 +0100
@@ -15,7 +15,7 @@
   echo "  Expand shorthand goal commands in FILES.  Also contracts uses of"
   echo "  resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on"
   echo "  1-element lists; furthermore expands tabs, since they are now"
-  echo "  forbidden in strings."
+  echo "  forbidden in ML string constants."
   echo
   echo "  Renames old versions of FILES by appending \"~~\"."
   echo