aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-08-12 12:57:33 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-08-12 12:57:33 +0000
commitaed209d2a59ee71f3f4a434e8c6a6166d48f2eee (patch)
tree74a4aa807d209035d5d40c47cde982384b84f0e8 /tools
parentd1519d9ac8dba8982e1701df7e16bb01487f445f (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-xtools/restore-v74
-rwxr-xr-xtools/upgrade-v88
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