ci: Don't run jobs again when pushing to master

We used to need this to get a correct code coverage report, but since we no longer merge using the buttons on the GitHub website, all our merges are fast-forward, and this should no longer be needed.
robinlinden · Dec 2, 2023 · eddd3e1 · eddd3e1
1 parent 32276bb
commit eddd3e1
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
@@ -1,8 +1,6 @@
 on:
   pull_request:
   workflow_dispatch:
-  push:
-    branches: [master]
 name: ci
 
 # https://docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions#permissions