From ae325798c95bd43126e72ce71a7e76e4bee69d3e Mon Sep 17 00:00:00 2001
From: Matej Košík <matej.kosik@inria.fr>
Date: Fri, 21 Jul 2017 15:48:23 +0200
Subject: make sure that API-leaks cannot be reintroduced by mistake

---
 Makefile.build | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index 7703df08f..e3316df91 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -564,6 +564,12 @@ kernel/kernel.cma: kernel/kernel.mllib
 	$(SHOW)'OCAMLC -a -o $@'
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(VMBYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
 
+# Specific rule for API/API.cmi
+# Make sure that API/API.mli cannot leak types from the Coq codebase.
+API/API.cmi : API/API.mli
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)$(OCAMLC) -I lib -I $(MYCAMLP4LIB) -c $<
+
 %.cma: %.mllib
 	$(SHOW)'OCAMLC -a -o $@'
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
-- 
cgit v1.2.3