aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-04-29 13:59:44 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2018-04-30 01:02:13 -0400
commit149aee10f5c4ff9ce8f29f2df2660fd38ac3ba7c (patch)
treece1c614f6b131f937768da985927b8609382b9e5 /Makefile
parent26a5193a11ace7de40ee2de134f29f51ba5845a6 (diff)
Only install files built by the coq target
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index e54fc39fa..9afb43291 100644
--- a/Makefile
+++ b/Makefile
@@ -95,6 +95,7 @@ SELECTED_PATTERN := \
SELECTED_SPECIFIC_PRE_VOFILES := $(filter $(SELECTED_PATTERN),$(REGULAR_VOFILES))
COQ_VOFILES := $(filter-out $(SPECIFIC_GENERATED_VOFILES),$(REGULAR_VOFILES))
+FILESTOINSTALL := $(filter-out $(SPECIFIC_GENERATED_VOFILES),$(FILESTOINSTALL))
SPECIFIC_VO := $(filter src/Specific/%,$(REGULAR_VOFILES))
NONAUTOGENERATED_SPECIFIC_VO := $(filter-out $(SPECIFIC_GENERATED_VOFILES),$(SPECIFIC_VO))
NON_SPECIFIC_VO := $(filter-out $(SPECIFIC_VO),$(REGULAR_VOFILES))