From 20f45f5644f82df437b09838a2fbdbfc7b6aa4e7 Mon Sep 17 00:00:00 2001
From: eine <eine@users.noreply.github.com>
Date: Fri, 5 Jun 2020 16:09:09 +0200
Subject: ci: dispatch after push to 'master' only

---
 .github/workflows/push.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml
index 9db20ff..3585ca0 100644
--- a/.github/workflows/push.yml
+++ b/.github/workflows/push.yml
@@ -18,6 +18,7 @@ jobs:
     - uses: actions/checkout@v1
     - run: ./ci.sh
     - name: Trigger 'synth' in ghdl/docker
+      if: github.ref == 'refs/heads/master' && github.event_name != 'pull_request'
       run: |
         curl -X POST https://api.github.com/repos/ghdl/docker/dispatches \
         -H "Content-Type: application/json" \
-- 
cgit v1.2.3