summaryrefslogtreecommitdiff
path: root/tools/check-v8
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /tools/check-v8
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'tools/check-v8')
-rwxr-xr-xtools/check-v824
1 files changed, 24 insertions, 0 deletions
diff --git a/tools/check-v8 b/tools/check-v8
new file mode 100755
index 00000000..9dfa0be3
--- /dev/null
+++ b/tools/check-v8
@@ -0,0 +1,24 @@
+#!/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 ----------------------