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)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 1211bc02128c95b5aa170e8761f6a915ef26e018..3c9459284d6c449fa05cc7768f06df55a30a9699 100644 (file)
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -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

diff --git a/.github/workflows/codeql-analysis.yml b/.github/workflows/codeql-analysis.yml
index 482eb5c13321f38a7e3ff58d07fa3315b999c178..6ec3f420e24a59a18470a7e26501d4b76d73d94f 100644 (file)
--- a/.github/workflows/codeql-analysis.yml
+++ b/.github/workflows/codeql-analysis.yml
@@ -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

diff --git a/src/version.c b/src/version.c
index dd99a31d35298102e92ea3d00fec3f88943aa58b..6d23fa8fc0f18f7ea1dc075271ad7c2e1782ef92 100644 (file)
--- a/src/version.c
+++ b/src/version.c
@@ -749,6 +749,8 @@ static char *(features[]) =
 
 static int included_patches[] =
 {   /* Add new patch number below this line */
+/**/
+    3891,
 /**/
     3890,
 /**/