Add .PRECIOUS directives for generated .cmi files

CertiCoq · Feb 15, 2024 · 3701f85 · 3701f85
1 parent 7af61ed
commit 3701f85
Showing 1 changed file with 6 additions and 5 deletions.
diff --git a/bootstrap/certicoqc/Makefile b/bootstrap/certicoqc/Makefile
@@ -73,9 +73,15 @@ theories/CertiCoqC.vo: theories/CertiCoqC.v
 theories/compile.vo: theories/compile.v theories/CertiCoqC.vo
  coqc ${COQOPTS} $<
 
+g_certicoqc.ml: g_certicoqc.mlg certicoqc.cmx certicoqc_plugin_wrapper.cmx
+ coqpp $<
+
+certicoqc.cmx: certicoqc_plugin_wrapper.cmx
+
 %.o: %.c theories/compile.vo
  $(CCOMPILER) $(CCOMPILEROPTS) -o $@ $<
 
+.PRECIOUS: %.cmi
 %.cmi: %.mli
  ocamlfind opt ${PKGS} ${OCAMLOPTS} -for-pack Certicoqc_plugin $<
 
@@ -91,13 +97,8 @@ certicoqc_plugin.cmx: certicoqc_plugin_wrapper.cmx certicoqc.cmx g_certicoqc.cmx
 certicoqc_plugin.cmxa: certicoqc_plugin.cmx
  ocamlfind opt -linkall ${OCAMLOPTS} -a -o $@ $<
 
-g_certicoqc.ml: g_certicoqc.mlg certicoqc.cmx certicoqc_plugin_wrapper.cmx
- coqpp $<
-
 certicoqc_wrapper.c: theories/compile.vo
 
-certicoqc.cmx: certicoqc_plugin_wrapper.cmx
-
 install: theories/compile.vo certicoqc_plugin.cmxs
  install -d "$(COQLIBINSTALL)"
  install -m 0644 theories/CertiCoqC.v theories/CertiCoqC.vo theories/compile.v theories/compile.vo certicoqc_plugin.cmx* "$(COQLIBINSTALL)"