make deploy: also do a push if we updated wiki links, to allow pulls

This commit is contained in:
Simon Michael 2018-05-16 11:58:08 -07:00
parent 0b5ff2906d
commit 38e7e378bd
2 changed files with 5 additions and 5 deletions

View File

@ -984,11 +984,11 @@ site/index.md: wiki/_Sidebar.md \
> site/_index.md.$$$$ && \
mv site/_index.md.$$$$ site/index.md
site/index.md-commit: \
$(call def-help,site/index.md, update home page with ./wiki/_Sidebar content and commit if changed )
site/index.md-push: \
$(call def-help,site/index.md-push, update home page with ./wiki/_Sidebar content and commit and do a git push if changed )
git diff --quiet site/index.md && \
make -s site/index.md && \
( git diff --quiet site/index.md || git commit -q -m 'site: home: update from wiki' -m '[ci skip]' site/index.md )
( git diff --quiet site/index.md || (git commit -q -m 'site: home: update from wiki' -m '[ci skip]' site/index.md && git push) )
site-clean: site/hakyll-std/hakyll-std \
$(call def-help,site-clean, remove hakyll-generated files (& take down the website) ) #cleanolddocs

View File

@ -19,8 +19,8 @@ echo && date --rfc-3339=seconds && \
# fetch latest wiki content
printf "wiki: " && git -C wiki pull && \
# add latest wiki sidebar links to home page
make --no-print-directory site/index.md-commit && \
# add latest wiki sidebar links to home page, and push right away so we can keep pulling
make --no-print-directory site/index.md-push && \
# ensure GHC can handle non-ascii
export LANG=en_US.UTF-8 && \