From 57898f9ba14f2f9a1a77f62cd7377527f7f470cf Mon Sep 17 00:00:00 2001
From: Alex Richardson <alexrichardson@google.com>
Date: Mon, 29 Jan 2024 14:38:55 -0800
Subject: [PATCH] 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 <alexrichardson@google.com>
---
 .github/workflows/build-pdf.yml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/build-pdf.yml b/.github/workflows/build-pdf.yml
index c2b75d2..e3c7e2b 100644
--- 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?