diff options
| author | Maxime Dénès | 2019-05-09 14:00:35 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-09 14:00:35 +0200 |
| commit | b2826206063c1ce596736a1e92550b4c24eaea71 (patch) | |
| tree | bddac014f8d88ca40a0ebf61e042a994c9d3647a | |
| parent | 0974a1efff523338a5f31f0a15492710bdc00658 (diff) | |
| parent | 86fa401ceaa17bdf1d297808eff3f8c3792d2778 (diff) | |
Merge PR #10082: Fix PLUGINSVO computation after ltac2 integration
Reviewed-by: maximedenes
| -rw-r--r-- | Makefile.vofiles | 2 |
1 files changed, 1 insertions, 1 deletions
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) |