From fc77555de9fda63cc7a1670716afbddca541921e Mon Sep 17 00:00:00 2001
From: Trevor Elliott <trevor@galois.com>
Date: Thu, 16 May 2013 14:41:34 -0700
Subject: more consistent redirection

---
 doc/build.mk | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

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)
-- 
cgit v1.2.3