diff options
Diffstat (limited to 'early-plugins.mk')
| -rw-r--r-- | early-plugins.mk | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/early-plugins.mk b/early-plugins.mk index 96b36d4..c8a9457 100644 --- a/early-plugins.mk +++ b/early-plugins.mk @@ -141,7 +141,10 @@ endif endif ifdef AUTO_CI_MASTER_MINS -ci:: $(KERL) +ci:: + $(verbose) $(MAKE) --no-print-directory ci-auto-master + +ci-auto-master: $(KERL) ifneq ($(wildcard $(KERL_INSTALL_DIR)/master),) $(verbose) if find $(KERL_INSTALL_DIR)/master/activate \ -mmin +$(AUTO_CI_MASTER_MINS) | grep -q master; then \ |