equal
deleted
inserted
replaced
13 echo "Usage: $PRG [FILES ...]" |
13 echo "Usage: $PRG [FILES ...]" |
14 echo |
14 echo |
15 echo " Expand shorthand goal commands in FILES. Also contracts uses of" |
15 echo " Expand shorthand goal commands in FILES. Also contracts uses of" |
16 echo " resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on" |
16 echo " resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on" |
17 echo " 1-element lists; furthermore expands tabs, since they are now" |
17 echo " 1-element lists; furthermore expands tabs, since they are now" |
18 echo " forbidden in strings." |
18 echo " forbidden in ML string constants." |
19 echo |
19 echo |
20 echo " Renames old versions of FILES by appending \"~~\"." |
20 echo " Renames old versions of FILES by appending \"~~\"." |
21 echo |
21 echo |
22 exit 1 |
22 exit 1 |
23 } |
23 } |