diff options
Diffstat (limited to 'src/doc/embedded-book/.github')
| -rw-r--r-- | src/doc/embedded-book/.github/bors.toml | 4 | ||||
| -rw-r--r-- | src/doc/embedded-book/.github/workflows/ci.yml | 8 |
2 files changed, 5 insertions, 7 deletions
diff --git a/src/doc/embedded-book/.github/bors.toml b/src/doc/embedded-book/.github/bors.toml deleted file mode 100644 index c3cfa378d..000000000 --- a/src/doc/embedded-book/.github/bors.toml +++ /dev/null @@ -1,4 +0,0 @@ -block_labels = ["needs-decision"] -delete_merged_branches = true -required_approvals = 1 -status = ["build"] diff --git a/src/doc/embedded-book/.github/workflows/ci.yml b/src/doc/embedded-book/.github/workflows/ci.yml index b1e3d552e..9018d1146 100644 --- a/src/doc/embedded-book/.github/workflows/ci.yml +++ b/src/doc/embedded-book/.github/workflows/ci.yml @@ -1,9 +1,11 @@ name: CI on: - push: - branches: [ staging, trying, master ] - pull_request: + push: # Run CI for all branches except GitHub merge queue tmp branches + branches-ignore: + - "gh-readonly-queue/**" + pull_request: # Run CI for PRs on any branch + merge_group: # Run CI for the GitHub merge queue jobs: build: |