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 ++++ 1 file changed, 4 insertions(+) (limited to 'Makefile') 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 -- cgit