diff options
author | Trevor Elliott <trevor@galois.com> | 2013-06-21 14:29:28 -0700 |
---|---|---|
committer | Trevor Elliott <trevor@galois.com> | 2013-06-21 14:40:26 -0700 |
commit | 4b9a4468238b96482478b3fabdfe6fb8cabb4fd6 (patch) | |
tree | c904129516281f7984cb350981843af3565bd35a /doc | |
parent | d538e07c07c6057126748ac9cccac3139600be5b (diff) |
Populate the gh-pages branch of the repo
Diffstat (limited to 'doc')
-rw-r--r-- | doc/build.mk | 22 |
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) |