From 96396b2e86d335f00efa932da861e4e4dc004a0b Mon Sep 17 00:00:00 2001
From: Christian Schwarz <me@cschwarz.com>
Date: Sat, 9 Sep 2023 11:07:01 +0000
Subject: [PATCH] circleci: fixup bc92660: docs/publish.sh script -P option
 didn't work

forgot to add it to getopt
---
 docs/publish.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/publish.sh b/docs/publish.sh
index c68956d..38e61de 100755
--- a/docs/publish.sh
+++ b/docs/publish.sh
@@ -4,7 +4,7 @@ set -euo pipefail
 NON_INTERACTIVE=false
 DO_CLONE=false
 PUSH=false
-while getopts "ca" arg; do
+while getopts "caP" arg; do
     case "$arg" in
         "a")
             NON_INTERACTIVE=true