From 324072c12a164f98d0ffa8125d319ffb49df87d8 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 31 Oct 2019 17:04:48 +0100
Subject: Communicate CFLAGS to dune

---
 kernel/byterun/dune | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'kernel')

diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index 20bdf28e54..d0145176ea 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -1,3 +1,16 @@
+; Dune doesn't use configure's output, but it is still necessary for
+; some Coq files to work; will be fixed in the future.
+(rule
+ (targets dune.c_flags)
+ (mode fallback)
+ (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX))
+ (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))
+
+(env
+ (dev     (c_flags (:include dune.c_flags)))
+ (release (c_flags (:include dune.c_flags)))
+ (ireport (c_flags (:include dune.c_flags))))
+
 (library
  (name byterun)
  (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
-- 
cgit v1.2.3