From 7c9b3828ab1d29ef50cb2c7756eadfb190804476 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 29 May 2013 13:09:51 +0000
Subject: Fix compilation of runtime system.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2263 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 Makefile         | 4 ++++
 runtime/Makefile | 4 ++--
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index 7357e5e..70f6013 100644
--- a/Makefile
+++ b/Makefile
@@ -122,7 +122,9 @@ all:
 	$(MAKE) proof
 	$(MAKE) extraction
 	$(MAKE) ccomp
+ifeq ($(HAS_RUNTIME_LIB),true)
 	$(MAKE) runtime
+endif
 ifeq ($(CCHECKLINK),true)
 	$(MAKE) cchecklink
 endif
@@ -225,7 +227,9 @@ install:
 ifeq ($(CCHECKLINK),true)
 	install ./cchecklink $(BINDIR)
 endif
+ifeq ($(HAS_RUNTIME_LIB),true)
 	$(MAKE) -C runtime install
+endif
 
 clean:
 	rm -f $(patsubst %, %/*.vo, $(DIRS))
diff --git a/runtime/Makefile b/runtime/Makefile
index cd4e301..81df4ea 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -14,10 +14,10 @@ $(LIB): $(OBJS)
 	ar rcs $(LIB) $(OBJS)
 
 %.o: $(ARCH)/%.s
-	$(CASMRUNTIME) $^
+	$(CASMRUNTIME) -o $@ $^
 
 %.o: $(ARCH)/%.S
-	$(CASMRUNTIME) -DVARIANT_$(VARIANT) -DSYS_$(SYSTEM) $^
+	$(CASMRUNTIME) -DVARIANT_$(VARIANT) -DSYS_$(SYSTEM) -o $@ $^
 
 clean::
 	rm -f *.o $(LIB)
-- 
cgit v1.2.3