From 86fa401ceaa17bdf1d297808eff3f8c3792d2778 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 7 May 2019 14:56:51 +0200
Subject: Fix PLUGINSVO computation after ltac2 integration

Avoid looking at random installed packages in -local mode.
---
 Makefile.vofiles | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.vofiles')

diff --git a/Makefile.vofiles b/Makefile.vofiles
index e05822c889..5296ed43ff 100644
--- a/Makefile.vofiles
+++ b/Makefile.vofiles
@@ -13,7 +13,7 @@ endif
 ###########################################################################
 
 THEORIESVO := $(patsubst %.v,%.$(VO),$(shell find theories -type f -name "*.v"))
-PLUGINSVO := $(patsubst %.v,%.$(VO),$(shell find plugins user-contrib -type f -name "*.v"))
+PLUGINSVO := $(patsubst %.v,%.$(VO),$(shell find plugins $(addprefix user-contrib/, $(USERCONTRIBDIRS)) -type f -name "*.v"))
 ALLVO := $(THEORIESVO) $(PLUGINSVO)
 VFILES := $(ALLVO:.$(VO)=.v)
 
-- 
cgit v1.2.3