equal
deleted
inserted
replaced
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. Also" |
15 echo " Recursively find .ML files, expand shorthand goal commands. Also" |
16 echo " contracts uses of resolve_tac, dresolve_tac, eresolve_tac," |
16 echo " contracts uses of resolve_tac, dresolve_tac, eresolve_tac," |
17 echo " forward_tac, rewrite_goals_tac on 1-element lists; furthermore expands" |
17 echo " forward_tac, rewrite_goals_tac on 1-element lists; furthermore" |
18 echo " tabs, which are forbidden in SML string constants." |
18 echo " expands 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 } |