corrected file name suffixes
authoroheimb
Tue, 30 Jan 2001 18:48:33 +0100
changeset 11001 6754fa0f2af7
parent 11000 498d0db8cd8a
child 11002 e33dfe9bde39
corrected file name suffixes
lib/Tools/convert
lib/scripts/convert.pl
--- 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
 }
--- 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");
   }
 }