From 99d46d24e0282c3e4c5fe8765f4e755a1b3b0253 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 1 Oct 2020 10:42:22 +0200 Subject: ccomp.force target for forcing compilation without Coq processing --- Makefile | 4 ++++ Makefile.extr | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/Makefile b/Makefile index adbfb661..5fc3997b 100644 --- a/Makefile +++ b/Makefile @@ -188,6 +188,10 @@ ccomp: .depend.extr compcert.ini driver/Version.ml FORCE ccomp.byte: .depend.extr compcert.ini driver/Version.ml FORCE $(MAKE) -f Makefile.extr ccomp.byte +# DM force compilation without checking dependencies +ccomp.force: .depend.extr compcert.ini driver/Version.ml FORCE + $(MAKE) -f Makefile.extr ccomp.force + clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE $(MAKE) -f Makefile.extr clightgen clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE diff --git a/Makefile.extr b/Makefile.extr index 1a894a16..75eb6dca 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -93,6 +93,10 @@ ccomp: $(CCOMP_OBJS) @echo "Linking $@" @$(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $+ +# DM force compilation without checking dependencies +ccomp.force: + $(OCAMLOPT) -o $@ $(LIBS) $(LINK_OPT) $(CCOMP_OBJS) + ccomp.byte: $(CCOMP_OBJS:.cmx=.cmo) @echo "Linking $@" @$(OCAMLC) -o $@ $(LIBS_BYTE) $+ -- cgit