aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/restore-v7
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-08-11 10:15:52 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-08-11 10:15:52 +0000
commit70015a2eba9dcbf15e00a2597400c6afba56523f (patch)
tree532e423cdbf522978df0db89b91f1baf04da0afa /tools/restore-v7
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/restore-v7')
-rwxr-xr-xtools/restore-v79
1 files changed, 9 insertions, 0 deletions
diff --git a/tools/restore-v7 b/tools/restore-v7
new file mode 100755
index 000000000..1115593ed
--- /dev/null
+++ b/tools/restore-v7
@@ -0,0 +1,9 @@
+#!/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
+ j=`echo $i | sed -e "s@^v7/@@"`
+ echo Restoring $i from v7
+ cp -f $i $j
+done