aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Benjamin Jones <bjones@galois.com>2012-10-30 11:38:33 -0700
committerGravatar Benjamin Jones <bjones@galois.com>2012-10-30 11:38:33 -0700
commite340601fb8422e8b94b09e003b71668e68cb6b54 (patch)
treee6335e547be7f290e4e04af1b8966febf1984ab4 /doc
parent00b39d16630cad9699c0eda6f5e1cedc535c7805 (diff)
added target: all
Diffstat (limited to 'doc')
-rw-r--r--doc/Makefile6
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/Makefile b/doc/Makefile
index e9539c1..7e3c32e 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -2,11 +2,13 @@ JSDOC_DIR=jsdoc
MANUAL_DIR=manual
MANUAL_SRC=manual_src
MAN_DEPS=$(MANUAL_SRC)/*.md $(MANUAL_SRC)/figures/*.png
+JSDOC_TOOLKIT=../build/jsdoc
-jsdoc-toolkit=../build/jsdoc
+all: jsdoc man
+.PHONY: jsdoc
jsdoc: ../contexts/data/fiveui/injected/prelude.js ../contexts/data/fiveui/injected/jquery-plugins.js
- @$(jsdoc-toolkit) ../contexts/data/fiveui/injected/prelude.js ../contexts/data/fiveui/injected/jquery-plugins.js
+ @$(JSDOC_TOOLKIT) ../contexts/data/fiveui/injected/prelude.js ../contexts/data/fiveui/injected/jquery-plugins.js
.PHONY: man
man: web-manual