aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-06-12 14:01:19 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-12 14:01:19 -0400
commit9f8372344ad923c730d0bb04fb84839c4fd59165 (patch)
treecfd52a1d952b43bcb745e5621e870eb1a3639f66 /Makefile
parent98e16a588e9a1b5918774415df06e346a113df8b (diff)
Handle multiple lite-unmade-vofiles
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 3e48c3e57..1a2599a87 100644
--- a/Makefile
+++ b/Makefile
@@ -63,7 +63,8 @@ DISPLAY_NON_JAVA_VO := $(filter-out $(DISPLAY_JAVA_VO),$(DISPLAY_VO))
# computing the vo_reverse_closure is slow, so we only do it if we're
# asked to make the lite target
ifneq ($(filter lite,$(MAKECMDGOALS)),)
-LITE_VOFILES := $(filter-out $(call vo_reverse_closure,$(VO_FILES),$(LITE_UNMADE_VOFILES)),$(COQ_VOFILES))
+LITE_ALL_UNMADE_VOFILES := $(foreach vo,$(LITE_UNMADE_VOFILES),$(call vo_reverse_closure,$(VOFILES),$(vo)))
+LITE_VOFILES := $(filter-out $(LITE_ALL_UNMADE_VOFILES),$(COQ_VOFILES))
endif
ifneq ($(filter only-heavy,$(MAKECMDGOALS)),)
HEAVY_VOFILES := $(call vo_closure,$(LITE_UNMADE_VOFILES))