<commit_before>#!/usr/bin/env bash

set -xe

# default value for NJOBS
: "${NJOBS:=1}"
export NJOBS

if [ -n "${GITLAB_CI}" ];
then
    export COQBIN="$PWD/_install_ci/bin"
    export CI_BRANCH="$CI_COMMIT_REF_NAME"
else
    if [ -n "${TRAVIS}" ];
    then
        export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST"
        export CI_BRANCH="$TRAVIS_BRANCH"
    elif [ -n "${CIRCLECI}" ];
    then
        export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
        export CI_BRANCH="$CIRCLE_BRANCH"
    fi
    export COQBIN="$PWD/bin"
fi
export PATH="$COQBIN:$PATH"

# Coq's tools need an ending slash :S, we should fix them.
export COQBIN="$COQBIN/"

ls "$COQBIN"

# Where we clone and build external developments
CI_BUILD_DIR="$PWD/_build_ci"

# shellcheck source=ci-basic-overlay.sh
source "${ci_dir}/ci-basic-overlay.sh"
for overlay in "${ci_dir}"/user-overlays/*.sh; do
    # shellcheck source=/dev/null
    source "${overlay}"
done

mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"

# git_checkout branch url dest will create a git repository
# in <dest> (if it does not exist already) and checkout the
# remote branch <branch> from <url>
git_checkout()
{
  local _BRANCH=${1}<commit_msg>ci-common: guess CI_BRANCH for local builds<commit_after>#!/usr/bin/env bash

set -xe

# default value for NJOBS
: "${NJOBS:=1}"
export NJOBS

if [ -n "${GITLAB_CI}" ];
then
    export COQBIN="$PWD/_install_ci/bin"
    export CI_BRANCH="$CI_COMMIT_REF_NAME"
else
    if [ -n "${TRAVIS}" ];
    then
        export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST"
        export CI_BRANCH="$TRAVIS_BRANCH"
    elif [ -n "${CIRCLECI}" ];
    then
        export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
        export CI_BRANCH="$CIRCLE_BRANCH"
    else # assume local
        export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
    fi
    export COQBIN="$PWD/bin"
fi
export PATH="$COQBIN:$PATH"

# Coq's tools need an ending slash :S, we should fix them.
export COQBIN="$COQBIN/"

ls "$COQBIN"

# Where we clone and build external developments
CI_BUILD_DIR="$PWD/_build_ci"

# shellcheck source=ci-basic-overlay.sh
source "${ci_dir}/ci-basic-overlay.sh"
for overlay in "${ci_dir}"/user-overlays/*.sh; do
    # shellcheck source=/dev/null
    source "${overlay}"
done

mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"

# git_checkout branch url dest will create a git repository
# in <dest> (if it does not exist already) and checkout the
# remote branch <branch> from <url>
git_checkout()
{
  local _BRANCH=${1}
{'fraction_non_alphanumeric': 0.13573743922204215, 'fraction_numerical': 0.0016207455429497568, 'mean_word_length': 3.938, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5131087', 'n_tokens_mistral': 946, 'n_tokens_neox': 903, 'n_words': 228}