equal
deleted
inserted
replaced
14 echo |
14 echo |
15 echo "Usage: $PRG [FILES|DIRS...]" |
15 echo "Usage: $PRG [FILES|DIRS...]" |
16 echo |
16 echo |
17 echo " Recursively find .thy/.ML files, patching them to ensure that" |
17 echo " Recursively find .thy/.ML files, patching them to ensure that" |
18 echo " dots in formulas are followed by non-idents." |
18 echo " dots in formulas are followed by non-idents." |
|
19 echo |
|
20 echo " Renames old versions of FILES by appending \"~~\"." |
19 echo |
21 echo |
20 exit 1 |
22 exit 1 |
21 } |
23 } |
22 |
24 |
23 |
25 |