equal
deleted
inserted
replaced
10 function usage() |
10 function usage() |
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: $PRG [FILES|DIRS...]" |
13 echo "Usage: $PRG [FILES|DIRS...]" |
14 echo |
14 echo |
15 echo " Recursively find .ML files, expand shorthand goal commands." |
15 echo " Recursively find .ML files, expand shorthand goal commands. Also" |
16 echo " Also contracts uses of resolve_tac, dresolve_tac, eresolve_tac," |
16 echo " contracts uses of resolve_tac, dresolve_tac, eresolve_tac," |
17 echo " rewrite_goals_tac on 1-element lists; furthermore expands tabs," |
17 echo " forward_tac, rewrite_goals_tac on 1-element lists; furthermore expands" |
18 echo " since they are now forbidden in ML string constants." |
18 echo " tabs, which are forbidden in SML 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 } |