From 3bad48d82b53f071ac41b79b5a9b896e26e6715c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 20 Apr 2022 14:36:03 +0200
Subject: [PATCH] Fixes Makefile for the reduc plugin.

---
 share/Makefile.config.in | 1 +
 1 file changed, 1 insertion(+)

diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index ed2c149f201..505153e2f1f 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@
-- 
GitLab