diff --git a/share/Makefile.config.in b/share/Makefile.config.in index ed2c149f201bb7ef37bc5f5d10e4402dd173519a..505153e2f1f6a9204002f5b82a59d777febce816 100644 --- a/share/Makefile.config.in +++ b/share/Makefile.config.in @@ -189,6 +189,7 @@ ENABLE_METRICS ?=@ENABLE_METRICS@ ENABLE_OCCURRENCE ?=@ENABLE_OCCURRENCE@ ENABLE_PDG ?=@ENABLE_PDG@ ENABLE_POSTDOMINATORS ?=@ENABLE_POSTDOMINATORS@ +ENABLE_REDUC ?=@ENABLE_REDUC@ ENABLE_RTEGEN ?=@ENABLE_RTEGEN@ ENABLE_SCOPE ?=@ENABLE_SCOPE@ ENABLE_SLICING ?=@ENABLE_SLICING@