diff options
Diffstat (limited to 'plugins/ci.mk')
| -rw-r--r-- | plugins/ci.mk | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/ci.mk b/plugins/ci.mk index 4f62132..4b902be 100644 --- a/plugins/ci.mk +++ b/plugins/ci.mk @@ -24,8 +24,10 @@ ci:: $(addprefix ci-,$(CI_OTP) $(addsuffix -native,$(CI_HIPE)) $(addsuffix -erll ci-prepare: $(addprefix $(KERL_INSTALL_DIR)/,$(CI_OTP) $(addsuffix -native,$(CI_HIPE))) ci-setup:: + $(verbose) : ci-extra:: + $(verbose) : ci_verbose_0 = @echo " CI " $(1); ci_verbose = $(ci_verbose_$(V)) |