From b49d809346bb420c7994c75fa0121f6d28870c05 Mon Sep 17 00:00:00 2001 From: Dario Nieuwenhuis Date: Thu, 24 Jul 2025 23:29:54 +0200 Subject: [PATCH] Add dedup to doc job. --- .github/ci/doc.sh | 2 ++ 1 file changed, 2 insertions(+) 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 @@ #!/bin/bash ## on push branch=main +## priority -10 +## dedup dequeue set -euxo pipefail