aboutsummaryrefslogtreecommitdiff
path: root/tools/upgrade-v8
diff options
context:
space:
mode:
authorherbelin2003-08-11 10:15:52 +0000
committerherbelin2003-08-11 10:15:52 +0000
commit70015a2eba9dcbf15e00a2597400c6afba56523f (patch)
tree532e423cdbf522978df0db89b91f1baf04da0afa /tools/upgrade-v8
parent9edb2d97d405ef15ca19af9021e664ef72bab5a6 (diff)
Outils de traduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4252 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/upgrade-v8')
-rwxr-xr-xtools/upgrade-v822
1 files changed, 22 insertions, 0 deletions
diff --git a/tools/upgrade-v8 b/tools/upgrade-v8
new file mode 100755
index 0000000000..513df2f223
--- /dev/null
+++ b/tools/upgrade-v8
@@ -0,0 +1,22 @@
+#!/bin/sh
+
+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
+ 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
+ j=v7/$i
+ mkdir -p `dirname $j`
+ mv -u -f $i $j
+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
+ j=`dirname $i`/`basename $i .v8`.v
+ echo Upgrading $i
+ mv -u -f $i $j
+done