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 @@
 #!/bin/bash
 ## on push branch=main
+## priority -10
+## dedup dequeue
 set -euxo pipefail

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