author | wenzelm |
Tue, 04 Nov 1997 17:16:26 +0100 | |
changeset 4130 | 9fac2370a2f4 |
parent 4129 | 2fd816aa6206 |
child 4131 | 916641b59219 |
--- a/lib/Tools/fixclasimp Tue Nov 04 17:12:13 1997 +0100 +++ b/lib/Tools/fixclasimp Tue Nov 04 17:16:26 1997 +0100 @@ -15,9 +15,7 @@ echo "Usage: $PRG [FILES|DIRS...]" echo echo " Recursively find .ML files, fixing references to" - echo " implicit claset and simpset:" - echo - echo " FIXME" + echo " implicit claset and simpset." echo echo " Renames old versions of FILES by appending \"~~\"." echo