run pipelines in GitHub mirror every time

it's pretty annoying to have to go the GitHub mirror and run pipelines manually...

see !202 (merged)

desired workflow

• open an MR here
• protect the associated branch when changes could affect pipeline runs
• push to the mirror, automatically because the branch is now protected
• run the pipeline on the pushed commits automatically => this is where the change should occur
• get the status of the pipelines with something like the following => maybe add a script for that

const GH_API_OPTIONS = [
    -H "Accept: application/vnd.github+json"
    -H "X-GitHub-Api-Version: 2022-11-28"
]
const GITHUB_MIRROR = "dragoon-rs/komodo"
let res = gh api ...$GH_API_OPTIONS $"/repos/($GITHUB_MIRROR)/actions/runs" | from json

let runs = $res.workflow_runs
    | where head_branch == <branch>
    | select id head_sha status conclusion run_started_at
    | into datetime run_started_at
    | sort-by run_started_at

$runs
    | update id { $"[`($in)`]\(https://github.com/($GITHUB_MIRROR)/actions/runs/($in)\)" }
    | update run_started_at { format date "%Y-%m-%dT%H:%M:%S" }
    | to md --pretty

and get something like

id	head_sha	status	conclusion	run_started_at
14237650542	d67f1cfd	completed	success	2025-04-03T07:44:14
14237741570	9ef598a1	completed	success	2025-04-03T07:49:40
14238086977	0a79edf3	completed	success	2025-04-03T08:09:13
14238175174	a84b2b12	in_progress		2025-04-03T08:13:52

added bookkeeping dev labels

assigned to @a.stevan

changed the description

mentioned in merge request !203 (merged)

closed with merge request !203 (merged)

mentioned in commit c462679e