diff options
| author | Dario Nieuwenhuis <[email protected]> | 2025-07-27 23:38:23 +0200 |
|---|---|---|
| committer | Dario Nieuwenhuis <[email protected]> | 2025-07-27 23:38:23 +0200 |
| commit | c708cefe03363135c466a3c0e8543a95973bce7a (patch) | |
| tree | 0f8d4440327521a151824bb77c995304c33fe623 /.github/ci/doc.sh | |
| parent | fee841e527588fffb773ff87bdfeaed28c514dfd (diff) | |
Add cooldown to doc, book jobs.
Diffstat (limited to '.github/ci/doc.sh')
| -rwxr-xr-x | .github/ci/doc.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.github/ci/doc.sh b/.github/ci/doc.sh index 26971afdc..ac96008d8 100755 --- a/.github/ci/doc.sh +++ b/.github/ci/doc.sh | |||
| @@ -2,6 +2,7 @@ | |||
| 2 | ## on push branch=main | 2 | ## on push branch=main |
| 3 | ## priority -100 | 3 | ## priority -100 |
| 4 | ## dedup dequeue | 4 | ## dedup dequeue |
| 5 | ## cooldown 15m | ||
| 5 | 6 | ||
| 6 | set -euxo pipefail | 7 | set -euxo pipefail |
| 7 | 8 | ||