lib/Tools/fixdots

--- a/lib/Tools/fixdots	Thu Oct 09 18:01:27 1997 +0200
+++ b/lib/Tools/fixdots	Fri Oct 10 14:51:58 1997 +0200
@@ -17,6 +17,8 @@
   echo "  Recursively find .thy/.ML files, patching them to ensure that"
   echo "  dots in formulas are followed by non-idents."
   echo
+  echo "  Renames old versions of FILES by appending \"~~\"."
+  echo
   exit 1
 }