diff options
| author | Dario Nieuwenhuis <[email protected]> | 2025-07-24 23:29:54 +0200 |
|---|---|---|
| committer | Dario Nieuwenhuis <[email protected]> | 2025-07-24 23:29:54 +0200 |
| commit | b49d809346bb420c7994c75fa0121f6d28870c05 (patch) | |
| tree | 76704df531782c5048bebf83feec67ade6d9c8d1 /.github | |
| parent | ff29d61b318efb54912096ec7771b0a906380440 (diff) | |
Add dedup to doc job.
Diffstat (limited to '.github')
| -rwxr-xr-x | .github/ci/doc.sh | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/.github/ci/doc.sh b/.github/ci/doc.sh index 90662af82..9162b37ae 100755 --- a/.github/ci/doc.sh +++ b/.github/ci/doc.sh | |||
| @@ -1,5 +1,7 @@ | |||
| 1 | #!/bin/bash | 1 | #!/bin/bash |
| 2 | ## on push branch=main | 2 | ## on push branch=main |
| 3 | ## priority -10 | ||
| 4 | ## dedup dequeue | ||
| 3 | 5 | ||
| 4 | set -euxo pipefail | 6 | set -euxo pipefail |
| 5 | 7 | ||