From 38e7e378bd0ed8490c966b7bfeaa64e9ae0db723 Mon Sep 17 00:00:00 2001 From: Simon Michael Date: Wed, 16 May 2018 11:58:08 -0700 Subject: [PATCH] make deploy: also do a push if we updated wiki links, to allow pulls --- Makefile | 6 +++--- tools/deploy.sh | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Makefile b/Makefile index 579c03c13..9fc3075ae 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/tools/deploy.sh b/tools/deploy.sh index fb58179a8..c18b8b259 100755 --- a/tools/deploy.sh +++ b/tools/deploy.sh @@ -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 && \