diff options
| author |  Rogan Creswick <creswick@gmail.com> | 2013-06-20 16:55:44 -0700 |
|---|---|---|
| committer | Rogan Creswick <creswick@gmail.com> | 2013-06-20 16:55:44 -0700 |
| commit | 5f92d9b352f0d1a3c7b94f5c41a6b582ae6e6ebc (patch) | |
| tree | feaa5b14d9199287707b25a0e275ff5c0a7ee39c /Makefile | |
| parent | 382e0245fa57502cbb9d58802c17e3079a44206d (diff) | |
| parent | fb7b4116ca156be854c19c114b015d975fea24ba (diff) | |
Merge branch 'master' of github.com:GaloisInc/FiveUI
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -90,7 +90,7 @@ else remote-url := $(shell $(git-cmd) config remote.origin.url) -$(build-dir)/gh-pages: $(topdir)/.git/index | $(build-dir) +$(build-dir)/gh-pages: | $(build-dir) $(call label,CLONE $(call drop-prefix,$@))\ ( $(git-cmd) clone $(if $(Q),-q) $(topdir) $@ \ && cd $@ \ @@ -107,6 +107,7 @@ generate: $(build-dir)/gh-pages/binaries/fiveui.xpi \ $(build-dir)/gh-pages/binaries/fiveui.crx $(call label,GENERATE)\ ( cd $(build-dir)/gh-pages \ + && $(git-cmd) pull $(if $(Q),-q) \ && $(git-cmd) add binaries \ && $(git-cmd) add -u binaries \ && $(git-cmd) commit $(if $(Q),-q) -m "deploy extensions" ) |