corrected file name suffixes
authoroheimb
Tue Jan 30 18:48:33 2001 +0100 (2001-01-30)
changeset 110016754fa0f2af7
parent 11000 498d0db8cd8a
child 11002 e33dfe9bde39
corrected file name suffixes
lib/Tools/convert
lib/scripts/convert.pl
     1.1 --- a/lib/Tools/convert	Tue Jan 30 18:47:00 2001 +0100
     1.2 +++ b/lib/Tools/convert	Tue Jan 30 18:48:33 2001 +0100
     1.3 @@ -20,7 +20,8 @@
     1.4    echo "  Isabelle/Isar tactic emulation."
     1.5    echo "  Note: conversion is only approximated, based on some heuristics."
     1.6    echo
     1.7 -  echo "  Renames new versions of FILES by appending \".thy\"."
     1.8 +  echo "  Renames old versions of FILES by appending \"~0~\"."
     1.9 +  echo "  Creates new versions of FILES by appending \".thy\"."
    1.10    echo
    1.11    exit 1
    1.12  }
     2.1 --- a/lib/scripts/convert.pl	Tue Jan 30 18:47:00 2001 +0100
     2.2 +++ b/lib/scripts/convert.pl	Tue Jan 30 18:48:33 2001 +0100
     2.3 @@ -152,7 +152,7 @@
     2.4        s/@@(\d+)@@/$thmnames[$1]/eg;
     2.5        print TMPW $_;
     2.6      }
     2.7 -    system("mv $currfile $currfile.~0~");
     2.8 +    system("mv $currfile $currfile~0~");
     2.9      system("rm $tmpfile");
    2.10    }
    2.11  }