From a74f6b45d72834b5b8417297017bd81424123d98 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 7 Mar 2010 15:52:58 +0000
Subject: 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
---
 coq | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'coq')

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
-- 
cgit v1.2.3