srctree

Robin Linden parent 32276bb8 eddd3e1d
ci: Don't run jobs again when pushing to master

We used to need this to get a correct code coverage report, but since weno longer merge using the buttons on the GitHub website, all our mergesare fast-forward, and this should no longer be needed.
inlinesplit
.github/workflows/ci.yaml added: 1, removed: 3, total 0
@@ -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