Use choice for revision_mark GitHub Actions input

This makes it easier to select one of the three options.
riscv · Jan 29, 2024 · f1705ad · f1705ad
1 parent d647a2a
commit f1705ad
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?