diff options
author | 2003-08-12 12:57:33 +0000 | |
---|---|---|
committer | 2003-08-12 12:57:33 +0000 | |
commit | aed209d2a59ee71f3f4a434e8c6a6166d48f2eee (patch) | |
tree | 74a4aa807d209035d5d40c47cde982384b84f0e8 /tools | |
parent | d1519d9ac8dba8982e1701df7e16bb01487f445f (diff) |
Bug et amliorations diverses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4263 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rwxr-xr-x | tools/restore-v7 | 4 | ||||
-rwxr-xr-x | tools/upgrade-v8 | 8 |
2 files changed, 6 insertions, 6 deletions
diff --git a/tools/restore-v7 b/tools/restore-v7 index 1115593ed..ab8845879 100755 --- a/tools/restore-v7 +++ b/tools/restore-v7 @@ -1,8 +1,8 @@ #!/bin/sh echo Restoring v7 files from directory v7 -for i in v7/*.v v7/*/*.v v7/*/*/*.v v7/*/*/*/*.v v7/*/*/*/*/*.v v7/*/*/*/*/*/*.v; do - if expr $i : '.*\*\.v' > /dev/null ; then continue ; fi +v7files=`find v7 -name \*.v` +for i in $v7files; do j=`echo $i | sed -e "s@^v7/@@"` echo Restoring $i from v7 cp -f $i $j diff --git a/tools/upgrade-v8 b/tools/upgrade-v8 index 513df2f22..443e70f26 100755 --- a/tools/upgrade-v8 +++ b/tools/upgrade-v8 @@ -3,8 +3,8 @@ mv v7 v7.bak echo ---------------- Saving v7 files into directory v7 ------------------ -for i in *.v */*.v */*/*.v */*/*/*.v */*/*/*/*.v */*/*/*/*/*.v; do - if expr $i : '.*\*\.v' > /dev/null ; then continue ; fi +vfiles=`find . -name \*.v` +for i in $files; do if expr $i : 'v7\.bak/.*\.v' > /dev/null ; then continue ; fi if expr $i : 'v7/.*\.v' > /dev/null ; then continue ; fi echo Saving $i into v7/$i @@ -14,8 +14,8 @@ for i in *.v */*.v */*/*.v */*/*/*.v */*/*/*/*.v */*/*/*/*/*.v; do done echo ---------------- Upgrading files with v8 syntax --------------------- -for i in *.v8 */*.v8 */*/*.v8 */*/*/*.v8 */*/*/*/*.v8 */*/*/*/*/*.v8; do - if expr $i : '.*\*\.v8' > /dev/null ; then continue ; fi +v8files=`find . -name \*.v8` +for i in $v8files; do j=`dirname $i`/`basename $i .v8`.v echo Upgrading $i mv -u -f $i $j |