aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-01-05 17:03:10 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-05-23 10:48:28 +0200
commitcd6dd06789139ee0ff5c2b79a280476999fe2bf1 (patch)
treee05396c2eb65ad5691172fa3b089236f6b5b233c
parent577f6d0e5c4eecca3a3cd46dfc37084123f4adf6 (diff)
print_config: print COQ_SRC_SUBDIRS
This way a makefile can just iterate on this list, intead of having a bunch of -I hardcoded in there by coq_makefile
-rw-r--r--lib/envars.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/envars.ml b/lib/envars.ml
index b20d39fb5..8654ee1a5 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -226,5 +226,7 @@ let print_config f =
fprintf f "CAMLP4BIN=%s/\n" (camlp4bin ());
fprintf f "CAMLP4LIB=%s\n" (camlp4lib ());
fprintf f "CAMLP4OPTIONS=%s\n" Coq_config.camlp4compat;
- fprintf f "HASNATDYNLINK=%s\n" (if Coq_config.has_natdynlink then "true" else "false")
+ fprintf f "HASNATDYNLINK=%s\n"
+ (if Coq_config.has_natdynlink then "true" else "false");
+ fprintf f "COQ_SRC_SUBDIRS=%s\n" (String.concat " " coq_src_subdirs)