Trigger Github workflow for merges

A merge is viewed by Github as a push to the branch where the merge
occurs, see https://github.community/t/trigger-workflow-only-on-pull-request-merge/17359/2
This means we should have coverage reports for merge commits from
Github, which should result in saner numbers.
parent 34b1893e
name: "Continuous Integration"
on:
pull_request:
on: ["pull_request", "push"]
jobs:
static-analysis-phpstan:
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment