diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-14 12:35:27 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-14 12:35:54 -0400 |
| commit | 33e49c00046bb8c988eec789bde89f3a6913542b (patch) | |
| tree | a56e38fee2d9783a1a9e2e224f5d5753c28c86c8 /Makefile | |
| parent | 0db89ececa4064256bedd1b2119230c2163b46fb (diff) | |
Error if Makefile.vo_closure doesn't exist and we need it
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -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 |