diff options
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -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)) |