aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-06-12 13:55:00 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-12 13:55:00 -0400
commit98e16a588e9a1b5918774415df06e346a113df8b (patch)
tree18b98b5e1e44f9d7a076e5f1646824298abfda1c /Makefile
parentd8437458af78868c80c519139691ce1a63d79ebb (diff)
Fix lite target (typo in makefile fn call)
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 612f7b656..3e48c3e57 100644
--- a/Makefile
+++ b/Makefile
@@ -60,10 +60,10 @@ SPECIFIC_DISPLAY_VO := $(filter src/Specific/%Display.vo,$(VOFILES))
DISPLAY_VO := $(SPECIFIC_DISPLAY_VO)
DISPLAY_JAVA_VO := $(filter %JavaDisplay.vo,$(DISPLAY_VO))
DISPLAY_NON_JAVA_VO := $(filter-out $(DISPLAY_JAVA_VO),$(DISPLAY_VO))
-# computing the reverse_vo_closure is slow, so we only do it if we're
+# 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 reverse_vo_closure,$(VO_FILES),$(LITE_UNMADE_VOFILES)),$(COQ_VOFILES))
+LITE_VOFILES := $(filter-out $(call vo_reverse_closure,$(VO_FILES),$(LITE_UNMADE_VOFILES)),$(COQ_VOFILES))
endif
ifneq ($(filter only-heavy,$(MAKECMDGOALS)),)
HEAVY_VOFILES := $(call vo_closure,$(LITE_UNMADE_VOFILES))