diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Makefile | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/Makefile b/lib/Makefile index 9ddf3a0544..71313170b0 100644 --- a/lib/Makefile +++ b/lib/Makefile @@ -52,6 +52,10 @@ else endif endif +# Any applications listed in SKIP-APPLICATIONS should be skipped +SKIP_FILE := $(wildcard SKIP-APPLICATIONS) +SKIP_APPLICATIONS := $(if $(SKIP_FILE),$(shell cat $(SKIP_FILE))) +SUB_DIRECTORIES := $(filter-out $(SKIP_APPLICATIONS),$(SUB_DIRECTORIES)) # ---------------------------------------------------------------------- include $(ERL_TOP)/make/otp_subdir.mk |