Add --delete-dockerfile to build.py script to not rmtree everytime

Author: nvuillam

.automation/build.py

@@ -46,6 +46,8 @@
 UPDATE_DEPENDENTS = "--dependents" in sys.argv
 UPDATE_CHANGELOG = "--changelog" in sys.argv
 IS_LATEST = "--latest" in sys.argv
+DELETE_DOCKERFILES = "--delete-dockerfiles" in sys.argv
+
 # Release args management
 if RELEASE is True:
     RELEASE_TAG = sys.argv[sys.argv.index("--release") + 1]
@@ -556,8 +558,8 @@ def match_flavor(item, flavor, flavor_info):
 # Automatically generate Dockerfile for standalone linters
 def generate_linter_dockerfiles():
     # Remove all the contents of LINTERS_DIR beforehand so that the result is deterministic
-    shutil.rmtree(os.path.realpath(LINTERS_DIR))
-    os.makedirs(os.path.realpath(LINTERS_DIR))
+    if DELETE_DOCKERFILES is True:
+        shutil.rmtree(os.path.realpath(LINTERS_DIR))
     # Browse descriptors
     linters_md = "# Standalone linter docker images\n\n"
     linters_md += "| Linter key | Docker image | Size |\n"

.github/workflows/deploy-DEV-linters.yml

@@ -22,7 +22,7 @@ on:
 # Set the Job #
 ###############
 concurrency:
-  group: '${{ github.workflow }} @ ${{ github.event.pull_request.head.label || github.head_ref || github.ref }}'
+  group: ${{ github.ref_name }}-${{ github.workflow }}
   cancel-in-progress: true
 
 jobs:

build.sh

@@ -1,8 +1,6 @@
 #!/usr/bin/env bash
 set -eu
 
-git config core.filemode false
-
 PYTHONPATH=.
 export PYTHONPATH
 if type python3 >/dev/null 2>/dev/null; then