# 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~~