diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-11 10:15:52 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-08-11 10:15:52 +0000 |
commit | 70015a2eba9dcbf15e00a2597400c6afba56523f (patch) | |
tree | 532e423cdbf522978df0db89b91f1baf04da0afa /tools/restore-v7 | |
parent | 9edb2d97d405ef15ca19af9021e664ef72bab5a6 (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-x | tools/restore-v7 | 9 |
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 |