Enable the PR CI job to be run manually (#215).

[ivanperez-keera]

The PR workflow CI job sometimes gets stuck, and there's no way to manually trigger it so that it completes. This prevents PRs from being merged.

This commit adjusts the conditions for the job to run so that it can be executed manually if needed.

[Bckempa]

I was kind of surprised to see the colons with no child attributes and since we don't have any child conditions of these triggers at the moment another valid syntax is on: [pull_request, workflow_dispatch], but if this works I'm happy with it.

How confident are we that a manual run will get picked up but a stuck PR?

[EzraBrooks]

This still puts the burden of the re-run onto the maintainers, since the average contributor can't hit this button. I would advise that we just use the typical strategy of putting up an empty commit temporarily to re-trigger the web hooks when we see GitHub lose an Action run.

[ivanperez-keera]

This still puts the burden of the re-run onto the maintainers

I disagree. It doesn't put the burden on the maintainers, it gives them a possibility that otherwise they would not have.

If you add an empty commit, either you have to merge a PR with an empty commit, which is just noise, or when you remove it, the PR and the repo don't match (the PR doesn't really check a commit that was merged).

I still disagree, but arguing would be a waste of time.

[EzraBrooks]

You're still seeing runner brownouts because of #219, which I opened #220 to fix.

[mkhansenbot]

@ivanperez-keera - Can we merge this?

[ivanperez-keera]

We've decided not to include this yet. We'll keep an eye to see if the problem really keeps happening and merge only in that case. Please do not scope this for any release yet.

[mkhansenbot]

Can we close this? If we're not going to merge it, then I think we should.