aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Trevor Elliott <trevor@galois.com>2013-06-21 14:29:28 -0700
committerGravatar Trevor Elliott <trevor@galois.com>2013-06-21 14:40:26 -0700
commit4b9a4468238b96482478b3fabdfe6fb8cabb4fd6 (patch)
treec904129516281f7984cb350981843af3565bd35a /doc
parentd538e07c07c6057126748ac9cccac3139600be5b (diff)
Populate the gh-pages branch of the repo
Diffstat (limited to 'doc')
-rw-r--r--doc/build.mk22
1 files changed, 22 insertions, 0 deletions
diff --git a/doc/build.mk b/doc/build.mk
index 79efa14..8015747 100644
--- a/doc/build.mk
+++ b/doc/build.mk
@@ -62,3 +62,25 @@ $(jsdoc-dir)/index.html: \
$(topdir)/src/js/fiveui/injected/jquery-plugins.js \
| $(build-dir)
$(call label,JSDOC)$(topdir)/tools/bin/jsdoc $^ $(redir)
+
+
+
+# Web Manual Publishing ########################################################
+
+generate: generate-docs
+
+.PHONY: generate-docs
+generate-docs: $(gh-pages-dir)/manual
+
+# this is a bit conservative, as it will copy the documentation through each
+# time the rule gets invoked. Some sort of a tag file to track actual changes
+# would be sufficient to not perform extra work.
+$(gh-pages-dir)/manual: DIR := $(manual-dir)
+$(gh-pages-dir)/manual: web-manual | pull-gh-pages
+ $(call cmd,copydir)
+
+generate-docs: $(gh-pages-dir)/jsdoc
+
+$(gh-pages-dir)/jsdoc: DIR := $(jsdoc-dir)
+$(gh-pages-dir)/jsdoc: $(jsdoc-dir)/index.html | pull-gh-pages
+ $(call cmd,copydir)