diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-06 02:29:48 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-06 02:29:48 -0400 |
| commit | 0cb3a8455cf3899a8a5179b6f15583187f98c424 (patch) | |
| tree | 6a87c74c841cfe8f34870e39774d3a9e74a7eb6c /Makefile | |
| parent | 8b99f9984343aa43b50c9ed722f159482930bdbe (diff) | |
Fix the printlite target
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -72,7 +72,7 @@ DISPLAY_JAVA_VO := $(filter %JavaDisplay.vo,$(DISPLAY_VO)) 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)),) +ifneq ($(filter printlite lite,$(MAKECMDGOALS)),) 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 |