diff options
author | 2003-08-12 12:57:33 +0000 | |
---|---|---|
committer | 2003-08-12 12:57:33 +0000 | |
commit | aed209d2a59ee71f3f4a434e8c6a6166d48f2eee (patch) | |
tree | 74a4aa807d209035d5d40c47cde982384b84f0e8 /tools/restore-v7 | |
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/restore-v7')
-rwxr-xr-x | tools/restore-v7 | 4 |
1 files changed, 2 insertions, 2 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 |