From: Jérémie Astor <astor.jeremie@wanadoo.fr>
Date: Fri, 21 Feb 2020 21:34:50 +0000 (+0100)
Subject: :wrench: push bot only on source change
X-Git-Tag: nightly~1782
X-Git-Url: http://10.10.0.4:5575/?a=commitdiff_plain;h=292eae9797cfa9383d0519c175382174e62c06ea;p=gwion.git

:wrench: push bot only on source change
---

diff --git a/.github/workflows/bot.yml b/.github/workflows/bot.yml
index dcafa513..75eeb544 100644
--- a/.github/workflows/bot.yml
+++ b/.github/workflows/bot.yml
@@ -17,7 +17,7 @@ jobs:
       run: |
         git clone https://github.com/fennecdjay/gwion-cinch-bot
         cd gwion-cinch-bot
-        [ -z "$(git diff "HEAD^" src)" ] && exit 0
+        [ -z "$(git diff "HEAD^" src ast util)" ] && exit 0
         git config --local user.email "action@github.com"
         git config --local user.name "GitHub Action"
         git commit --allow-empty -m "update gwion"