summaryrefslogtreecommitdiff
path: root/Makefile.config.in
diff options
context:
space:
mode:
authorTom Kelly <ctk21@cl.cam.ac.uk>2021-10-01 12:19:35 +0100
committerTom Kelly <ctk21@cl.cam.ac.uk>2021-10-01 12:19:35 +0100
commitd85f4d8efd39ca4094930c179d233dbf85f44451 (patch)
tree6ce479f7abd09db85412345a467da95e01b4089d /Makefile.config.in
parentec296cb5f2d62b56c73197d71e60ec7850363bba (diff)
parent099b86a046e304fe15e2bb37557bffc6aafaab15 (diff)
downloadocaml-d85f4d8efd39ca4094930c179d233dbf85f44451.tar.gz
Merge commit '099b86a046e304fe15e2bb37557bffc6aafaab15' into parallel_minor_gc_4_13
Diffstat (limited to 'Makefile.config.in')
-rw-r--r--Makefile.config.in1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.config.in b/Makefile.config.in
index d386ceb426..590db7d87e 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -239,6 +239,7 @@ HOST=@host@
FLAMBDA=@flambda@
WITH_FLAMBDA_INVARIANTS=@flambda_invariants@
FORCE_INSTRUMENTED_RUNTIME=@force_instrumented_runtime@
+WITH_CMM_INVARIANTS=@cmm_invariants@
FORCE_SAFE_STRING=@force_safe_string@
DEFAULT_SAFE_STRING=@default_safe_string@
WINDOWS_UNICODE=@windows_unicode@