diff options
| author |  Trevor Elliott <trevor@galois.com> | 2013-06-03 11:03:57 -0700 |
|---|---|---|
| committer | Trevor Elliott <trevor@galois.com> | 2013-06-03 11:03:57 -0700 |
| commit | ad61ab21a854080c19fd5043fb9faf8586697e4f (patch) | |
| tree | c76e1fafb86db87642082ec6bac978b55cc35f17 /doc | |
| parent | dc44db4a3e35f655b6f1a22ecdbedb8b3aae64be (diff) | |
Switch documentation from the all target to a doc target
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/build.mk | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/doc/build.mk b/doc/build.mk index 09e447e..f62ef54 100644 --- a/doc/build.mk +++ b/doc/build.mk @@ -1,4 +1,7 @@ +.PHONY: doc +doc: + jsdoc-dir := $(build-dir)/jsdoc manual-dir := $(build-dir)/manual manual-src := $(path)/manual_src @@ -23,7 +26,7 @@ $(manual-deps): $(manual-dir)/%.html: $(manual-src)/%.md | $(manual-dir) # HTML Manual ################################################################## ifneq "$(pandoc)" "" -all: web-manual +doc: web-manual else $(warning pandoc not found, not building the manual) endif @@ -54,7 +57,7 @@ $(eval $(call stage-doc-dir,$(path)/images)) # JsDoc Documentation ########################################################## -all: $(jsdoc-dir)/index.html +doc: $(jsdoc-dir)/index.html $(jsdoc-dir)/index.html: \ $(topdir)/contexts/data/fiveui/injected/prelude.js \ |