lib/Tools/fixclasimp
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