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

ivanperez-keera · mkhansenbot · commit 16c5adea3416 · 2025-04-28T14:22:04.000-07:00
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.
diff --git a/.github/workflows/pr.yaml b/.github/workflows/pr.yaml
@@ -1,4 +1,5 @@
 on:
+  workflow_dispatch:
   pull_request:
 
 jobs:

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,5 @@`
`1`	`1`	`on:`
	`2`	`+ workflow_dispatch:`
`2`	`3`	`pull_request:`
`3`	`4`
`4`	`5`	`jobs:`