diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-05-15 19:25:37 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-05-15 19:25:55 -0400 |
| commit | 7bd5848deee3dab2a8df73f649588747a0f4caeb (patch) | |
| tree | 84d26ab9c6b93b24773c5eca5592c44e7ab3243c /Makefile | |
| parent | fb5b1fc36c1e967a3bad3ec6260e60c8c4770c9d (diff) | |
Fix a bug in previous commit
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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 |