From d0bffb62c890634697ff5c989829f17b615293fb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 19 Jun 2020 11:43:32 +0200
Subject: [PATCH] [Dive] Adds PLUGIN_ENABLE and PLUGIN_DISTRIBUTED to the
 Makefile.

---
 src/plugins/dive/Makefile.in | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/plugins/dive/Makefile.in b/src/plugins/dive/Makefile.in
index c4b5b76d4eb..1609a95d317 100644
--- a/src/plugins/dive/Makefile.in
+++ b/src/plugins/dive/Makefile.in
@@ -37,6 +37,7 @@ endif
 #########################
 
 PLUGIN_DIR ?=.
+PLUGIN_ENABLE:=@ENABLE_DIVE@
 PLUGIN_NAME := Dive
 PLUGIN_CMO := self callstack node_kind imprecision_graph build main \
   server_interface
@@ -46,6 +47,7 @@ PLUGIN_HAS_MLI:= yes
 PLUGIN_TESTS_DIRS:=dive
 PLUGIN_GENERATED:=
 PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
+PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
 
 ################
 # Generic part #
-- 
GitLab