# HG changeset patch
# User wenzelm
# Date 854026665 -3600
# Node ID 7288532f537259009c9ed44be647a8d5d7337483
# Parent  8669576160697c43c8c46a7714ff2ac244d68a4b
tuned;

diff -r 866957616069 -r 7288532f5372 lib/Tools/expandshort
--- a/lib/Tools/expandshort	Thu Jan 23 14:35:15 1997 +0100
+++ b/lib/Tools/expandshort	Thu Jan 23 14:37:45 1997 +0100
@@ -12,12 +12,12 @@
   echo
   echo "Usage: $PRG [FILES ...]"
   echo
-  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 "  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
-  echo "Renames old versions of FILES by appending \"~~\"."
+  echo "  Renames old versions of FILES by appending \"~~\"."
   echo
   exit 1
 }
@@ -31,6 +31,8 @@
 
 ## main
 
+[ "$1" = "-?" ] && usage
+
 for f in "$@"
 do
 echo Expanding shorthands in $f. \ Backup file is $f~~