shake site: also commit & push home page when wiki links change

[ci skip]
This commit is contained in:
Simon Michael 2019-03-06 09:18:52 -08:00
parent 7af5ee4863
commit e5f3dd1a75

View File

@ -471,6 +471,15 @@ main = do
-- update wiki links on website front page
need [ "site/index.md" ]
-- if it changed, commit (and push) it.
-- XXX the push will cause another webhook invocation of this script, try to avoid
cmd_ Shell
"git diff --quiet -- site/index.md"
"|| ("
"git commit -m ';site: home: wiki links' -m '[ci skip]' site/index.md"
"&& git push"
")"
-- update the live site based on all latest content
need [ "website-all" ]