lib/Tools/expandshort
changeset 2547 7288532f5372
parent 2546 866957616069
child 2588 b472d703fa06
--- 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~~