diff options
| -rw-r--r-- | .github/CODEOWNERS | 4 | ||||
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 10 |
2 files changed, 11 insertions, 3 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 3a762b42a..eb2797101 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -186,6 +186,10 @@ /pretyping/ @mattam82 # Secondary maintainer @gares +/pretyping/vnorm.* @maximedenes +/pretyping/nativenorm.* @maximedenes +# Secondary maintainer @ppedrot + ########## Pretty printer ########## /printing/ @herbelin diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index a4e60744f..94e90bf4f 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1437,12 +1437,16 @@ function make_addon_equations { } function make_addons { - if [ -n "${GITLAB_CI}" ]; then + if [ -n "$GITLAB_CI" ]; then export CI_BRANCH="$CI_COMMIT_REF_NAME" - if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]] - then + if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then export CI_PULL_REQUEST="${CI_BRANCH#pr-}" + else + export CI_PULL_REQUEST="" fi + else + export CI_BRANCH="" + export CI_PULL_REQUEST="" fi . /build/ci-basic-overlay.sh for overlay in /build/user-overlays/*.sh; do |