Merge of the newmem and newextcalls branches:

- Revised memory model with concrete representation of ints & floats,
  and per-byte access permissions
- Revised Globalenvs implementation
- Matching changes in all languages and proofs.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 11 insertions, 1 deletions

diff --git a/coq b/coq
index 19edb9a..97d4ca6 100755
--- a/coq
+++ b/coq
@@ -1,7 +1,17 @@
 #!/bin/sh
 # Start coqide with the right -I options
+# Use the Makefile to rebuild dependencies if needed
+# Recompile the modified file after coqide editing
 
 ARCH=`sed -n -e 's/^ARCH=//p' Makefile.config`
 VARIANT=`sed -n -e 's/^VARIANT=//p' Makefile.config`
 
-coqide -I lib -I common -I $ARCH/$VARIANT -I $ARCH -I backend -I cfrontend $1 && make ${1}o
+make -q ${1}o || {
+  make -n ${1}o | grep -v "\\b${1}\\b" | \
+  (while read cmd; do
+    $cmd || exit 2
+   done)
+}
+
+coqide -I lib -I common -I $ARCH/$VARIANT -I $ARCH -I backend -I cfrontend $1 \
+&& make ${1}o