diff options
| author |  Trevor Elliott <trevor@galois.com> | 2013-05-16 14:41:34 -0700 |
|---|---|---|
| committer | Trevor Elliott <trevor@galois.com> | 2013-05-16 14:41:34 -0700 |
| commit | fc77555de9fda63cc7a1670716afbddca541921e (patch) | |
| tree | f890bab387896160a6950f95e966e13f6b8f2620 | |
| parent | d316614847c16569da34a42e808dfb332fc6b6c9 (diff) | |
more consistent redirection
| -rw-r--r-- | contexts/build.mk | 2 | ||||
| -rw-r--r-- | doc/build.mk | 2 | ||||
| -rw-r--r-- | mk/util.mk | 2 |
3 files changed, 4 insertions, 2 deletions
diff --git a/contexts/build.mk b/contexts/build.mk index dba7701..7d43987 100644 --- a/contexts/build.mk +++ b/contexts/build.mk @@ -89,7 +89,7 @@ $(build-dir)/fiveui.crx: $(target-dir)/chrome-background.js \ && $(topdir)/tools/bin/makecrx stage \ $(topdir)/contexts/chrome/fiveui.pem \ fiveui \ - $(if $(Q),1>/dev/null) ) + $(redir) ) # install the extension manifest in the stage directory diff --git a/doc/build.mk b/doc/build.mk index 136048b..d13a22a 100644 --- a/doc/build.mk +++ b/doc/build.mk @@ -59,4 +59,4 @@ all: | $(jsdoc-dir) $(jsdoc-dir): $(topdir)/contexts/data/fiveui/injected/prelude.js \ $(topdir)/contexts/data/fiveui/injected/jquery-plugins.js \ | $(build-dir) - $(call label,JSDOC)$(topdir)/tools/bin/jsdoc $^ $(if $(Q),>/dev/null) + $(call label,JSDOC)$(topdir)/tools/bin/jsdoc $^ $(redir) @@ -2,9 +2,11 @@ ifneq "$(V)" "1" Q := @ quiet := quiet_ +redir := >/dev/null else Q := quiet := +redir := endif echo-cmd = $(if $($(quiet)cmd_$1),echo ' $($(quiet)cmd_$1)';) |