adminer/zrepl_patched
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

circleci: fixup bc92660: docs/publish.sh script -P option didn't work

Browse Source 
forgot to add it to getopt
This commit is contained in:
Christian Schwarz
2023-09-09 11:07:01 +00:00
parent 8749f0bd3d
commit 96396b2e86
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/publish.sh
+1 -1
View File
@@ -4,7 +4,7 @@ set -euo pipefail
NON_INTERACTIVE=false NON_INTERACTIVE=false
DO_CLONE=false DO_CLONE=false
PUSH=false PUSH=false
while getopts "ca" arg; do while getopts "caP" arg; do
case "$arg" in case "$arg" in
"a") "a")
NON_INTERACTIVE=true NON_INTERACTIVE=true