aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile.extr
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-02-19 16:24:28 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-02-19 16:24:28 +0100
commite51ffb6c1d9411515facc5e97a4e8dba5d8b55ab (patch)
tree80a7fc8212d28712365082e1a2a2d0fa28cedad3 /Makefile.extr
parentc130f4936bad11fd6dab3a5d142b870d2a5f650c (diff)
parentb0eb1dfc9fd7b15c556c49101390d882b0f00f8a (diff)
downloadcompcert-e51ffb6c1d9411515facc5e97a4e8dba5d8b55ab.tar.gz
compcert-e51ffb6c1d9411515facc5e97a4e8dba5d8b55ab.zip
Merge branch 'master' into no-shell
Diffstat (limited to 'Makefile.extr')
-rw-r--r--Makefile.extr8
1 files changed, 6 insertions, 2 deletions
diff --git a/Makefile.extr b/Makefile.extr
index 5c9cc8dd..3e46eb26 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -91,11 +91,11 @@ CCOMP_OBJS:=$(shell $(MODORDER) driver/Driver.cmx)
ccomp: $(CCOMP_OBJS)
@echo "Linking $@"
- @$(OCAMLOPT) -o $@ $(LIBS) $+
+ @$(OCAMLOPT) -o $@ $(LIBS) $+ $(LINKERSPEC)
ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo)
@echo "Linking $@"
- @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+
+ @$(OCAMLC) -o $@ $(LIBS:.cmxa=.cma) $+ $(LINKERSPEC)
ifeq ($(CCHECKLINK),true)
@@ -157,6 +157,10 @@ clean:
rm -f $(GENERATED)
for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done
+cleansource:
+ rm -f $(EXECUTABLES)
+ for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done
+
# Generation of .depend.extr
depend: $(GENERATED)