diff options
Diffstat (limited to 'tools/translate-v8')
-rwxr-xr-x | tools/translate-v8 | 41 |
1 files changed, 0 insertions, 41 deletions
diff --git a/tools/translate-v8 b/tools/translate-v8 deleted file mode 100755 index 7d71bea9..00000000 --- a/tools/translate-v8 +++ /dev/null @@ -1,41 +0,0 @@ -#!/bin/sh - -if [ -e v7 ]; then - echo "Warning: v7 directory found, the files are maybe already translated"; - sleep 5; -fi -echo --------- Producing v8 files in the translation directory ------------- -if [ -e v8 ]; then rm -r v8; fi -if [ -e /tmp/v7.$$ ]; then rm -r /tmp/v7.$$; fi -cp -pr . /tmp/v7.$$ -cp -pr /tmp/v7.$$ v8 -cd v8 -rm description toto -make clean -make COQFLAGS='-translate -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \ - { echo ---- Failed to translate; exit 1; } -echo --------- Upgrading files in the translation directory ---------------- -v8files=`find . -name \*.v8` -for i in $v8files; do - j=`dirname $i`/`basename $i .v8`.v - echo Upgrading $j in the translation directory - mv -u -f $i $j -done -echo --------- Recompiling v8 files in the translation directory ----------- -make clean -make || { echo ---- Failed to recompile; exit 1; } -echo --------- Saving v7 files in directory v7 ----------------------------- -/bin/rm -r ../v7 -mv /tmp/v7.$$ ../v7 -echo Saving v7 files done -echo --------- Upgrading files in current directory ------------------------ -vfiles=`find . -name \*.v` -cd .. -for i in $vfiles; do - echo Upgrading $i in current directory - mv -u -f v8/$i $i -done -echo --------- Translation completed --------------------------------------- -echo Old files are in directory '"v7"' -echo New files are in current directory -echo You can now remove the translation directory '"v8"' |