diff options
Diffstat (limited to 'Makefile.extr')
-rw-r--r-- | Makefile.extr | 8 |
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) |