From 91b77e55d63c60a2ee6fdfe9a02aafe95f976006 Mon Sep 17 00:00:00 2001 From: trag1c Date: Tue, 3 Feb 2026 23:12:43 +0100 Subject: [PATCH] add an optional PR number input for manual tip releases needed for the future GitHub bot to track comment-triggered PR builds --- .github/workflows/release-tip.yml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.github/workflows/release-tip.yml b/.github/workflows/release-tip.yml index d9fe4e5a8..324aab6f9 100644 --- a/.github/workflows/release-tip.yml +++ b/.github/workflows/release-tip.yml @@ -4,7 +4,11 @@ on: types: [completed] branches: [main] - workflow_dispatch: {} + workflow_dispatch: + inputs: + pr: + type: number + required: false name: Release Tip