Use an option input for revision_mark

This makes the GitHub UI show a dropdown box instead of text field. Signed-off-by: Alex Richardson <[email protected]>
riscv · Jan 29, 2024 · 57898f9 · 57898f9
1 parent e1c38be
commit 57898f9
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/.github/workflows/build-pdf.yml b/.github/workflows/build-pdf.yml
@@ -12,7 +12,11 @@ on:
       revision_mark:
         description: 'Set revision mark as Draft, Release or Stable:'
         required: true
-        type: string
+        type: choice
+        options:
+          - Draft
+          - Release
+          - Stable
         default: Draft
       prerelease:
         description: Tag as a pre-release?