aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-04-20 18:53:14 -0400
committerGravatar Jason Gross <jgross@mit.edu>2018-04-20 18:53:14 -0400
commit40e4751aa2b59f31504d2886a128b195899fe85d (patch)
treea439d488f6ceb0778ef4ef532159bdab3d80d504 /Makefile
parent281d1b9dfe269e1ad27d065d208acbdc3631dffb (diff)
Fix the lite-display target
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index b8989ace4..5492ca1a9 100644
--- a/Makefile
+++ b/Makefile
@@ -133,7 +133,7 @@ specific: $(SPECIFIC_VO) coqprime
non-specific: $(NON_SPECIFIC_VO) coqprime
coq: $(COQ_VOFILES) coqprime
lite: $(LITE_VOFILES) coqprime
-lite-display: $(LITE_DISPLAY_VOFILES:Display.vo=.log) coqprime
+lite-display: $(LITE_DISPLAY_VOFILES:.vo=.log) coqprime
only-heavy: $(HEAVY_VOFILES) coqprime
curves-proofs: $(CURVES_PROOFS_VOFILES) coqprime
no-curves-proofs: $(NO_CURVES_PROOFS_VOFILES) coqprime