From 99d46d24e0282c3e4c5fe8765f4e755a1b3b0253 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 1 Oct 2020 10:42:22 +0200
Subject: ccomp.force target for forcing compilation without Coq processing

---
 Makefile.extr | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Makefile.extr')

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