diff options
| author | herbelin | 2006-01-11 18:52:41 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-11 18:52:41 +0000 |
| commit | 9d26b73255b86ec710d8a59c8f196f96229b17c9 (patch) | |
| tree | abd1264f0c7b280c8ea7d06025da636b25b3db5b /tools/restore-v7 | |
| parent | bd2ec17a7948da7dff830b4411dbf823534a790c (diff) | |
Suppression traducteur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7846 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/restore-v7')
| -rwxr-xr-x | tools/restore-v7 | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/tools/restore-v7 b/tools/restore-v7 deleted file mode 100755 index ab88458796..0000000000 --- a/tools/restore-v7 +++ /dev/null @@ -1,9 +0,0 @@ -#!/bin/sh - -echo Restoring v7 files from directory v7 -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 -done |