patch 8.2.3891: github CI: workflows may overlap
Problem: Github CI: workflows may overlap.
Solution: Cancel previous workflows when starting a new one. (Yegappan
Lakshmanan, closes #9400)
This commit is contained in:
committed by
Bram Moolenaar
parent
d787e40fdb
commit
7f4a628efe
7
.github/workflows/ci.yml
vendored
7
.github/workflows/ci.yml
vendored
@ -5,6 +5,13 @@ on:
|
||||
branches: ['**']
|
||||
pull_request:
|
||||
|
||||
# Cancels all previous workflow runs for pull requests that have not completed.
|
||||
concurrency:
|
||||
# The concurrency group contains the workflow name and the branch name for
|
||||
# pull requests or the commit hash for any other events.
|
||||
group: ${{ github.workflow }}-${{ github.event_name == 'pull_request' && github.head_ref || github.sha }}
|
||||
cancel-in-progress: true
|
||||
|
||||
jobs:
|
||||
linux:
|
||||
runs-on: ubuntu-18.04
|
||||
|
||||
7
.github/workflows/codeql-analysis.yml
vendored
7
.github/workflows/codeql-analysis.yml
vendored
@ -14,6 +14,13 @@ on:
|
||||
schedule:
|
||||
- cron: '0 18 * * 1'
|
||||
|
||||
# Cancels all previous workflow runs for pull requests that have not completed.
|
||||
concurrency:
|
||||
# The concurrency group contains the workflow name and the branch name for
|
||||
# pull requests or the commit hash for any other events.
|
||||
group: ${{ github.workflow }}-${{ github.event_name == 'pull_request' && github.head_ref || github.sha }}
|
||||
cancel-in-progress: true
|
||||
|
||||
jobs:
|
||||
analyze:
|
||||
name: Analyze
|
||||
|
||||
@ -749,6 +749,8 @@ static char *(features[]) =
|
||||
|
||||
static int included_patches[] =
|
||||
{ /* Add new patch number below this line */
|
||||
/**/
|
||||
3891,
|
||||
/**/
|
||||
3890,
|
||||
/**/
|
||||
|
||||
Reference in New Issue
Block a user