From e5f3dd1a75da10ea5c4db43d15711a099b988d16 Mon Sep 17 00:00:00 2001 From: Simon Michael Date: Wed, 6 Mar 2019 09:18:52 -0800 Subject: [PATCH] shake site: also commit & push home page when wiki links change [ci skip] --- Shake.hs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Shake.hs b/Shake.hs index ee6bf3929..9c2aafe15 100755 --- a/Shake.hs +++ b/Shake.hs @@ -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" ]