Nouvelle version qui compile dans un sous-repertoire avant d'ecraser le repertoire courant

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5087 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 37 insertions, 11 deletions

diff --git a/tools/translate-v8 b/tools/translate-v8
index 1bf6e0bf5..7d71bea99 100755
--- a/tools/translate-v8
+++ b/tools/translate-v8
@@ -1,15 +1,41 @@
-echo
-echo ------------------ Producing v8 files -------------------------
+#!/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; }
-$COQBIN/../tools/upgrade-v8 || { echo ---- Failed to upgrade files; exit 1; }
-echo
-echo ------------------ Recompiling v8 files -----------------------
+ { 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
-echo ------------------ Translation completed ----------------------
-echo Old files are in directory v7
-
-
+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"'