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/upgrade-v8 | |
| 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/upgrade-v8')
| -rwxr-xr-x | tools/upgrade-v8 | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/tools/upgrade-v8 b/tools/upgrade-v8 deleted file mode 100755 index 36d0bf8c21..0000000000 --- a/tools/upgrade-v8 +++ /dev/null @@ -1,22 +0,0 @@ -#!/bin/sh - -mv v7 v7.bak - -echo ---------------- Saving v7 files into directory v7 ------------------ -vfiles=`find . -name \*.v` -for i in $vfiles; do - 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 --------------------- -v8files=`find . -name \*.v8` -for i in $v8files; do - j=`dirname $i`/`basename $i .v8`.v - echo Upgrading $i - mv -u -f $i $j -done |
