From 9f8372344ad923c730d0bb04fb84839c4fd59165 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 12 Jun 2017 14:01:19 -0400 Subject: Handle multiple lite-unmade-vofiles --- Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'Makefile') 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)) -- cgit v1.2.3