diff options
| author |  Rogan Creswick <creswick@galois.com> | 2012-03-30 17:07:02 -0700 |
|---|---|---|
| committer | Rogan Creswick <creswick@galois.com> | 2012-03-30 17:07:02 -0700 |
| commit | f6ab6622aab00fe7c2f4c3dc41f786ebbe0f0d73 (patch) | |
| tree | 870111038542cd27153e1396ebdc063573249689 /doc/Makefile | |
initial revision
Diffstat (limited to 'doc/Makefile')
| -rw-r--r-- | doc/Makefile | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/doc/Makefile b/doc/Makefile new file mode 100644 index 0000000..6d0fc25 --- /dev/null +++ b/doc/Makefile @@ -0,0 +1,26 @@ +JSDOC_DIR=jsdoc +MANUAL_DIR=manual +MANUAL_SRC=manual_src +MAN_DEPS=$(MANUAL_SRC)/*.md $(MANUAL_SRC)/figures/*.png + +jsdoc-toolkit=../build/jsdoc + +jsdoc: ../contexts/data/fiveui/injected/prelude.js + @$(jsdoc-toolkit) ../contexts/data/fiveui/injected/prelude.js + +.PHONY: man +man: web-manual + +$(MANUAL_DIR): + @mkdir -p $(MANUAL_DIR) + +.PHONY: web-manual +web-manual: $(MANUAL_DIR) $(MAN_DEPS) + @make -C $(MANUAL_SRC) + @cp -r $(MANUAL_SRC)/figures $(MANUAL_DIR) + @mv $(MANUAL_SRC)/*.html $(MANUAL_DIR) + +clean: + @make -C $(MANUAL_SRC) clean + @$(RM) -r $(JSDOC_DIR) + @$(RM) -r $(MANUAL_DIR) |