summaryrefslogtreecommitdiff
path: root/tools/check-v8
diff options
context:
space:
mode:
Diffstat (limited to 'tools/check-v8')
-rwxr-xr-xtools/check-v824
1 files changed, 0 insertions, 24 deletions
diff --git a/tools/check-v8 b/tools/check-v8
deleted file mode 100755
index 9dfa0be3..00000000
--- a/tools/check-v8
+++ /dev/null
@@ -1,24 +0,0 @@
-#!/bin/sh
-
-echo ------------------ Producing v8 files -------------------------
-if [ -e v8 ]; then rm -r v8; fi
-if [ -e /tmp/v8.$$ ]; then rm -r /tmp/v8.$$; fi
-cp -pr . /tmp/v8.$$
-mv /tmp/v8.$$ v8
-cd v8
-rm description
-make clean
-make COQFLAGS='-translate -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \
- { echo ---- Failed to translate; exit 1; }
-echo ------------------ Upgrading v8 files -------------------------
-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
-echo ------------------ Recompiling v8 files -----------------------
-make clean
-make || { echo ---- Failed to recompile; exit 1; }
-make clean # to save disk space
-echo ------------------ Translation completed ----------------------