# HG changeset patch
# User oheimb
# Date 980876913 -3600
# Node ID 6754fa0f2af72cae6e116de0d46b5bcd638eb26c
# Parent  498d0db8cd8a8ce227ba5b0d72713647509452d3
corrected file name suffixes

diff -r 498d0db8cd8a -r 6754fa0f2af7 lib/Tools/convert
--- a/lib/Tools/convert	Tue Jan 30 18:47:00 2001 +0100
+++ b/lib/Tools/convert	Tue Jan 30 18:48:33 2001 +0100
@@ -20,7 +20,8 @@
   echo "  Isabelle/Isar tactic emulation."
   echo "  Note: conversion is only approximated, based on some heuristics."
   echo
-  echo "  Renames new versions of FILES by appending \".thy\"."
+  echo "  Renames old versions of FILES by appending \"~0~\"."
+  echo "  Creates new versions of FILES by appending \".thy\"."
   echo
   exit 1
 }
diff -r 498d0db8cd8a -r 6754fa0f2af7 lib/scripts/convert.pl
--- a/lib/scripts/convert.pl	Tue Jan 30 18:47:00 2001 +0100
+++ b/lib/scripts/convert.pl	Tue Jan 30 18:48:33 2001 +0100
@@ -152,7 +152,7 @@
       s/@@(\d+)@@/$thmnames[$1]/eg;
       print TMPW $_;
     }
-    system("mv $currfile $currfile.~0~");
+    system("mv $currfile $currfile~0~");
     system("rm $tmpfile");
   }
 }