Silences “Warning: 1 issue was detected with this workflow: Please
make sure that every branch in on.pull_request is also in on.push so
that Code Scanning can compare pull requests against the state of the
base branch.”
Signed-off-by: Anders Kaseorg <anders@zulip.com>
We’ve always been running CI on both push events and pull_request
events, which means it runs twice for commits that are pushed to a
pull request.
Filter the push events by branch name. Add the workflow_dispatch
event in case developers want to manually run CI on some other branch
that isn’t a pull request.
https://docs.github.com/en/actions/managing-workflow-runs/manually-running-a-workflow
Signed-off-by: Anders Kaseorg <anders@zulip.com>
Since we already run this on every push we don't need to run it as a
cron job every week for no reason. While we are touching this code
block, we convert it to on: [push, pull_request] since the previous
format felt weird. It was only written that way because we had the
cron job declared there.
This file was generated by GitHub's code analysis tutorial; we were
just approved from their waitlist.
I deleted the part to run compilers as it is not relevant for us.
Anders Kaseorg
Alex Vandiver
Priyank Patel
Tim Abbott