Skip to content

Add workflow_dispatch

This is for the GitHub CI. It adds the necessary workflow_dispatch trigger to the GH workflow so that I can manually trigger a build on any branch; see https://build5nines.com/configuring-manual-triggers-in-github-actions-with-workflow_dispatch/.

Merge request reports