add an optional PR number input for manual tip releases

needed for the future GitHub bot to track
comment-triggered PR builds
This commit is contained in:
trag1c
2026-02-03 23:12:43 +01:00
parent 51897c0cd5
commit 91b77e55d6

View File

@@ -4,7 +4,11 @@ on:
types: [completed]
branches: [main]
workflow_dispatch: {}
workflow_dispatch:
inputs:
pr:
type: number
required: false
name: Release Tip