aboutsummaryrefslogtreecommitdiff
path: root/tools/check-v8
diff options
context:
space:
mode:
authorherbelin2006-01-11 18:52:41 +0000
committerherbelin2006-01-11 18:52:41 +0000
commit9d26b73255b86ec710d8a59c8f196f96229b17c9 (patch)
treeabd1264f0c7b280c8ea7d06025da636b25b3db5b /tools/check-v8
parentbd2ec17a7948da7dff830b4411dbf823534a790c (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/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 9dfa0be35e..0000000000
--- 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 ----------------------