diff options
Diffstat (limited to '.github/ci/doc.sh')
| -rwxr-xr-x | .github/ci/doc.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.github/ci/doc.sh b/.github/ci/doc.sh index 9162b37ae..26971afdc 100755 --- a/.github/ci/doc.sh +++ b/.github/ci/doc.sh | |||
| @@ -1,6 +1,6 @@ | |||
| 1 | #!/bin/bash | 1 | #!/bin/bash |
| 2 | ## on push branch=main | 2 | ## on push branch=main |
| 3 | ## priority -10 | 3 | ## priority -100 |
| 4 | ## dedup dequeue | 4 | ## dedup dequeue |
| 5 | 5 | ||
| 6 | set -euxo pipefail | 6 | set -euxo pipefail |