Skip to content
Snippets Groups Projects
Commit d0bffb62 authored by David Bühler's avatar David Bühler
Browse files

[Dive] Adds PLUGIN_ENABLE and PLUGIN_DISTRIBUTED to the Makefile.

parent 3f5d6490
No related branches found
No related tags found
No related merge requests found
......@@ -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 #
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment