diff options
author | Rogan Creswick <creswick@gmail.com> | 2013-06-25 10:44:43 -0700 |
---|---|---|
committer | Rogan Creswick <creswick@gmail.com> | 2013-06-25 10:44:43 -0700 |
commit | e166ed04bfe336f9e6340f7df1a50264f7d64622 (patch) | |
tree | b2be288c69240e444ec70ece945f0ec59e667690 /mk/gh-pages.mk | |
parent | 750bb02df87cb2731ee593b3206f1ac442fcd69d (diff) | |
parent | 50e042c8981608e4121f94faec138db0c3e294e3 (diff) |
Merge branch 'master' of https://github.com/GaloisInc/FiveUI
Diffstat (limited to 'mk/gh-pages.mk')
-rw-r--r-- | mk/gh-pages.mk | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/mk/gh-pages.mk b/mk/gh-pages.mk new file mode 100644 index 0000000..cfa67c5 --- /dev/null +++ b/mk/gh-pages.mk @@ -0,0 +1,53 @@ + +# gh-pages Branch Management ################################################### + +gh-pages-dir := $(build-dir)/gh-pages + +ifeq "$(git-cmd)" "" +$(call strict-error,"unable to locate git") +else + +# figure out the url of the origin that the current work repo uses +remote-url := $(shell $(git-cmd) config remote.origin.url) + +endif + + +# Pull in the gh-pages directory. +.PHONY: pull-gh-pages +ifeq "$(pull)" "0" +pull-gh-pages: +else +pull-gh-pages: | $(gh-pages-dir) + $(call label,PULL $(call drop-prefix,$(gh-pages-dir)))\ + ( cd $(gh-pages-dir) \ + && $(git-cmd) pull $(if $(Q),-q) ) +endif + + +# checkout the gh-pages branch in a temp repo under the build tree +$(gh-pages-dir): | $(build-dir) + $(call label,CLONE $(call drop-prefix,$@))\ + ( $(git-cmd) clone $(if $(Q),-q) $(topdir) $@ \ + && cd $(gh-pages-dir) \ + && $(git-cmd) remote set-url origin $(remote-url) \ + && $(git-cmd) fetch $(if $(Q),-q) origin gh-pages \ + && $(git-cmd) checkout $(if $(Q),-q) gh-pages ) + + +# Generate a commit in the gh-pages-dir, after adding some files that may have +# changed. +commit = $(call label,COMMIT $(call drop-prefix,$(gh-pages-dir)))\ + ( cd $(gh-pages-dir) \ + && if test -n "`$(git-cmd) status -s`"; then \ + $(git-cmd) add $1 \ + && $(git-cmd) commit $(if $(Q),-q) -m $2 \ + ; fi ) + + + +# push to the gh-pages branch from the temp repo +deploy: | pull-gh-pages + $(call label,DEPLOY)\ + ( cd $(gh-pages-dir) \ + && git push $(if $(Q),-q) origin gh-pages ) |