1 files changed, 4 insertions, 0 deletions
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