diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-12 20:27:33 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-12 20:27:33 +0000 |
commit | 8efaddd7df1603091fa27a10ad7c184b4241bebb (patch) | |
tree | a39223578ddbeed3a4a90df5aa2511a6964747d0 /tools | |
parent | f2af4dc98cd6785eb01b74fdb10e57dde05cec35 (diff) |
Outil de test de la traduction et de la compilation en v8 sans modification des
sources
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4393 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rwxr-xr-x | tools/check-v8 | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/tools/check-v8 b/tools/check-v8 new file mode 100755 index 000000000..30ab7aed2 --- /dev/null +++ b/tools/check-v8 @@ -0,0 +1,23 @@ +#!/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 OPT=-translate || { 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 OPT=-v8 || { echo ---- Failed to recompile; exit 1; } +make clean # to save disk space +echo ------------------ Translation completed ---------------------- |