diff options
author | Benjamin Jones <bjones@galois.com> | 2012-10-30 11:38:33 -0700 |
---|---|---|
committer | Benjamin Jones <bjones@galois.com> | 2012-10-30 11:38:33 -0700 |
commit | e340601fb8422e8b94b09e003b71668e68cb6b54 (patch) | |
tree | e6335e547be7f290e4e04af1b8966febf1984ab4 /doc | |
parent | 00b39d16630cad9699c0eda6f5e1cedc535c7805 (diff) |
added target: all
Diffstat (limited to 'doc')
-rw-r--r-- | doc/Makefile | 6 |
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 |