File tree 8 files changed +0
-112
lines changed
8 files changed +0
-112
lines changed Original file line number Diff line number Diff line change 4
4
push :
5
5
merge_group :
6
6
7
- # When pushing branches (and/or updating PRs), we do want to cancel previous
8
- # build runs. We assume they are stale now; and do not want to spend CI time and
9
- # resources on continuing to continue those runs. This is what the concurrency.group
10
- # value lets us express. When using merge queues, we now have to consider
11
- # - runs triggers by commits per pull-request
12
- # we want to cancel any previous run. So they should all get the same group (per PR)
13
- # - runs refs/heads/gh-readonly-queue/<target branch name> (they should all get their
14
- # unique git ref, we don't want to cancel any of the ones in the queue)
15
- # - if it's neither, we fall back to the run_id (this is a unique number for each
16
- # workflow run; it does not change if you "rerun" a job)
17
- concurrency :
18
- group : ${{ github.workflow }}-${{ github.event.type }}-${{ startsWith(github.ref, 'refs/heads/gh-readonly-queue/') && github.ref || github.event.pull_request.number || github.run_id }}
19
- cancel-in-progress : true
20
-
21
7
jobs :
22
8
check-cabal-files :
23
9
runs-on : ubuntu-latest
Original file line number Diff line number Diff line change 4
4
push :
5
5
merge_group :
6
6
7
- # When pushing branches (and/or updating PRs), we do want to cancel previous
8
- # build runs. We assume they are stale now; and do not want to spend CI time and
9
- # resources on continuing to continue those runs. This is what the concurrency.group
10
- # value lets us express. When using merge queues, we now have to consider
11
- # - runs triggers by commits per pull-request
12
- # we want to cancel any previous run. So they should all get the same group (per PR)
13
- # - runs refs/heads/gh-readonly-queue/<target branch name> (they should all get their
14
- # unique git ref, we don't want to cancel any of the ones in the queue)
15
- # - if it's neither, we fall back to the run_id (this is a unique number for each
16
- # workflow run; it does not change if you "rerun" a job)
17
- concurrency :
18
- group : ${{ github.workflow }}-${{ github.event.type }}-${{ startsWith(github.ref, 'refs/heads/gh-readonly-queue/') && github.ref || github.event.pull_request.number || github.run_id }}
19
- cancel-in-progress : true
20
-
21
7
jobs :
22
8
build :
23
9
runs-on : ubuntu-latest
Original file line number Diff line number Diff line change 4
4
push :
5
5
merge_group :
6
6
7
- # When pushing branches (and/or updating PRs), we do want to cancel previous
8
- # build runs. We assume they are stale now; and do not want to spend CI time and
9
- # resources on continuing to continue those runs. This is what the concurrency.group
10
- # value lets us express. When using merge queues, we now have to consider
11
- # - runs triggers by commits per pull-request
12
- # we want to cancel any previous run. So they should all get the same group (per PR)
13
- # - runs refs/heads/gh-readonly-queue/<target branch name> (they should all get their
14
- # unique git ref, we don't want to cancel any of the ones in the queue)
15
- # - if it's neither, we fall back to the run_id (this is a unique number for each
16
- # workflow run; it does not change if you "rerun" a job)
17
- concurrency :
18
- group : ${{ github.workflow }}-${{ github.event.type }}-${{ startsWith(github.ref, 'refs/heads/gh-readonly-queue/') && github.ref || github.event.pull_request.number || github.run_id }}
19
- cancel-in-progress : true
20
-
21
7
jobs :
22
8
build :
23
9
runs-on : ubuntu-latest
Original file line number Diff line number Diff line change 4
4
push :
5
5
merge_group :
6
6
7
- # When pushing branches (and/or updating PRs), we do want to cancel previous
8
- # build runs. We assume they are stale now; and do not want to spend CI time and
9
- # resources on continuing to continue those runs. This is what the concurrency.group
10
- # value lets us express. When using merge queues, we now have to consider
11
- # - runs triggers by commits per pull-request
12
- # we want to cancel any previous run. So they should all get the same group (per PR)
13
- # - runs refs/heads/gh-readonly-queue/<target branch name> (they should all get their
14
- # unique git ref, we don't want to cancel any of the ones in the queue)
15
- # - if it's neither, we fall back to the run_id (this is a unique number for each
16
- # workflow run; it does not change if you "rerun" a job)
17
- concurrency :
18
- group : ${{ github.workflow }}-${{ github.event.type }}-${{ startsWith(github.ref, 'refs/heads/gh-readonly-queue/') && github.ref || github.event.pull_request.number || github.run_id }}
19
- cancel-in-progress : true
20
-
21
7
jobs :
22
8
build :
23
9
runs-on : ubuntu-latest
Original file line number Diff line number Diff line change 4
4
push :
5
5
merge_group :
6
6
7
- # When pushing branches (and/or updating PRs), we do want to cancel previous
8
- # build runs. We assume they are stale now; and do not want to spend CI time and
9
- # resources on continuing to continue those runs. This is what the concurrency.group
10
- # value lets us express. When using merge queues, we now have to consider
11
- # - runs triggers by commits per pull-request
12
- # we want to cancel any previous run. So they should all get the same group (per PR)
13
- # - runs refs/heads/gh-readonly-queue/<target branch name> (they should all get their
14
- # unique git ref, we don't want to cancel any of the ones in the queue)
15
- # - if it's neither, we fall back to the run_id (this is a unique number for each
16
- # workflow run; it does not change if you "rerun" a job)
17
- concurrency :
18
- group : ${{ github.workflow }}-${{ github.event.type }}-${{ startsWith(github.ref, 'refs/heads/gh-readonly-queue/') && github.ref || github.event.pull_request.number || github.run_id }}
19
- cancel-in-progress : true
20
-
21
7
jobs :
22
8
build :
23
9
runs-on : ubuntu-latest
Original file line number Diff line number Diff line change 4
4
push :
5
5
merge_group :
6
6
7
- # When pushing branches (and/or updating PRs), we do want to cancel previous
8
- # build runs. We assume they are stale now; and do not want to spend CI time and
9
- # resources on continuing to continue those runs. This is what the concurrency.group
10
- # value lets us express. When using merge queues, we now have to consider
11
- # - runs triggers by commits per pull-request
12
- # we want to cancel any previous run. So they should all get the same group (per PR)
13
- # - runs refs/heads/gh-readonly-queue/<target branch name> (they should all get their
14
- # unique git ref, we don't want to cancel any of the ones in the queue)
15
- # - if it's neither, we fall back to the run_id (this is a unique number for each
16
- # workflow run; it does not change if you "rerun" a job)
17
- concurrency :
18
- group : ${{ github.workflow }}-${{ github.event.type }}-${{ startsWith(github.ref, 'refs/heads/gh-readonly-queue/') && github.ref || github.event.pull_request.number || github.run_id }}
19
- cancel-in-progress : true
20
-
21
7
jobs :
22
8
linux_ci :
23
9
runs-on : ${{ matrix.os }}
Original file line number Diff line number Diff line change 4
4
push :
5
5
merge_group :
6
6
7
- # When pushing branches (and/or updating PRs), we do want to cancel previous
8
- # build runs. We assume they are stale now; and do not want to spend CI time and
9
- # resources on continuing to continue those runs. This is what the concurrency.group
10
- # value lets us express. When using merge queues, we now have to consider
11
- # - runs triggers by commits per pull-request
12
- # we want to cancel any previous run. So they should all get the same group (per PR)
13
- # - runs refs/heads/gh-readonly-queue/<target branch name> (they should all get their
14
- # unique git ref, we don't want to cancel any of the ones in the queue)
15
- # - if it's neither, we fall back to the run_id (this is a unique number for each
16
- # workflow run; it does not change if you "rerun" a job)
17
- concurrency :
18
- group : ${{ github.workflow }}-${{ github.event.type }}-${{ startsWith(github.ref, 'refs/heads/gh-readonly-queue/') && github.ref || github.event.pull_request.number || github.run_id }}
19
- cancel-in-progress : true
20
-
21
7
jobs :
22
8
build :
23
9
runs-on : ${{ matrix.os }}
Original file line number Diff line number Diff line change 4
4
push :
5
5
merge_group :
6
6
7
- # When pushing branches (and/or updating PRs), we do want to cancel previous
8
- # build runs. We assume they are stale now; and do not want to spend CI time and
9
- # resources on continuing to continue those runs. This is what the concurrency.group
10
- # value lets us express. When using merge queues, we now have to consider
11
- # - runs triggers by commits per pull-request
12
- # we want to cancel any previous run. So they should all get the same group (per PR)
13
- # - runs refs/heads/gh-readonly-queue/<target branch name> (they should all get their
14
- # unique git ref, we don't want to cancel any of the ones in the queue)
15
- # - if it's neither, we fall back to the run_id (this is a unique number for each
16
- # workflow run; it does not change if you "rerun" a job)
17
- concurrency :
18
- group : ${{ github.workflow }}-${{ github.event.type }}-${{ startsWith(github.ref, 'refs/heads/gh-readonly-queue/') && github.ref || github.event.pull_request.number || github.run_id }}
19
- cancel-in-progress : true
20
-
21
7
jobs :
22
8
markdown-link-check :
23
9
runs-on : ubuntu-latest
You can’t perform that action at this time.
0 commit comments