From 33e49c00046bb8c988eec789bde89f3a6913542b Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 14 Jun 2017 12:35:27 -0400
Subject: Error if Makefile.vo_closure doesn't exist and we need it

---
 Makefile | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 1a2599a87..b52741ef4 100644
--- a/Makefile
+++ b/Makefile
@@ -37,7 +37,11 @@ COQ_VERSION := $(firstword $(subst $(COQ_VERSION_PREFIX),,$(shell "$(COQBIN)coqc
 -include Makefile.coq
 endif
 
+ifeq ($(filter lite only-heavy printdeps printreversedeps,$(MAKECMDGOALS)),)
 -include etc/coq-scripts/Makefile.vo_closure
+else
+include etc/coq-scripts/Makefile.vo_closure
+endif
 
 .DEFAULT_GOAL := coq
 
-- 
cgit v1.2.3