From 7bd5848deee3dab2a8df73f649588747a0f4caeb Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 15 May 2018 19:25:37 -0400 Subject: Fix a bug in previous commit --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 6da34ddab..368070341 100644 --- a/Makefile +++ b/Makefile @@ -116,7 +116,7 @@ LITE_ALL_UNMADE_VOFILES := $(foreach vo,$(LITE_UNMADE_VOFILES),$(call vo_reverse LITE_VOFILES := $(filter-out $(LITE_ALL_UNMADE_VOFILES),$(COQ_VOFILES)) LITE_DISPLAY_VOFILES := $(filter-out $(LITE_ALL_UNMADE_VOFILES),$(DISPLAY_VO)) endif -ifneq ($(filter nobigmem print-nobibmem,$(MAKECMDGOALS),) +ifneq ($(filter nobigmem print-nobigmem,$(MAKECMDGOALS)),) NOBIGMEM_ALL_UNMADE_VOFILES := $(foreach vo,$(NOBIGMEM_UNMADE_VOFILES),$(call vo_reverse_closure,$(VOFILES),$(vo))) NOBIGMEM_VOFILES := $(filter-out $(NOBIGMEM_ALL_UNMADE_VOFILES),$(COQ_VOFILES)) endif -- cgit v1.2.3