changeset 4130 | 9fac2370a2f4 |
parent 4077 | 8ce7c713968c |
child 4508 | f102cb0140fe |
--- 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