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"'