From 7bac5a91f8ea9ad0023f29200f8362a5eed02706 Mon Sep 17 00:00:00 2001 From: Vincent Laviron Date: Tue, 20 Apr 2021 09:24:48 +0200 Subject: Add --enable-cmm-invariants configure flag --- Makefile.config.in | 1 + 1 file changed, 1 insertion(+) (limited to 'Makefile.config.in') diff --git a/Makefile.config.in b/Makefile.config.in index 5ab44cd984..99445ebeb5 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -234,6 +234,7 @@ TARGET=@target@ HOST=@host@ FLAMBDA=@flambda@ WITH_FLAMBDA_INVARIANTS=@flambda_invariants@ +WITH_CMM_INVARIANTS=@cmm_invariants@ FORCE_SAFE_STRING=@force_safe_string@ DEFAULT_SAFE_STRING=@default_safe_string@ WINDOWS_UNICODE=@windows_unicode@ -- cgit v1.2.1