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 /doc | |
| parent | d316614847c16569da34a42e808dfb332fc6b6c9 (diff) | |
more consistent redirection
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/build.mk | 2 |
1 files changed, 1 insertions, 1 deletions
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) |