lib/Tools/fixdots
changeset 3826 0caedb36900d
parent 3825 478461d77e88
child 4508 f102cb0140fe
     1.1 --- a/lib/Tools/fixdots	Thu Oct 09 18:01:27 1997 +0200
     1.2 +++ b/lib/Tools/fixdots	Fri Oct 10 14:51:58 1997 +0200
     1.3 @@ -17,6 +17,8 @@
     1.4    echo "  Recursively find .thy/.ML files, patching them to ensure that"
     1.5    echo "  dots in formulas are followed by non-idents."
     1.6    echo
     1.7 +  echo "  Renames old versions of FILES by appending \"~~\"."
     1.8 +  echo
     1.9    exit 1
    1.10  }
    1.11