diff --git a/src/plugins/dive/Makefile.in b/src/plugins/dive/Makefile.in index c4b5b76d4ebd24d5079b2f275873c66fc25a1166..1609a95d3178f2a00f289b029af915220d16f2e6 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 #