diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-06-13 18:24:45 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-06-16 10:35:37 +0200 |
commit | d06af26e6cd93c6bb819b38573603a5e1121ed68 (patch) | |
tree | a4d6c02072d0626daa955ba3327e565c8399e1b9 | |
parent | e1d68573015883301cb401861e10233f6442d9ec (diff) |
Each user overlay goes into its own file.
This will avoid stupid merge conflicts in the future.
-rw-r--r-- | dev/ci/ci-common.sh | 4 | ||||
-rw-r--r-- | dev/ci/ci-user-overlay.sh | 58 | ||||
-rw-r--r-- | dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh | 4 | ||||
-rw-r--r-- | dev/ci/user-overlays/README.md | 14 |
4 files changed, 21 insertions, 59 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index f1e1515d4..5435e9588 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -18,7 +18,9 @@ ls "$COQBIN" # Where we clone and build external developments CI_BUILD_DIR=`pwd`/_build_ci -source ${ci_dir}/ci-user-overlay.sh +for overlay in ${ci_dir}/user-overlays/*.sh; do + source ${overlay} +done source ${ci_dir}/ci-basic-overlay.sh mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh deleted file mode 100644 index 2ecd40416..000000000 --- a/dev/ci/ci-user-overlay.sh +++ /dev/null @@ -1,58 +0,0 @@ -#!/usr/bin/env bash - -# Add user overlays here. You can use some logic to detect if you are -# in your travis branch and conditionally enable the overlay. - -# Some useful Travis variables: -# (https://docs.travis-ci.com/user/environment-variables/#Default-Environment-Variables) -# -# - TRAVIS_BRANCH: For builds not triggered by a pull request this is -# the name of the branch currently being built; whereas for builds -# triggered by a pull request this is the name of the branch -# targeted by the pull request (in many cases this will be master). -# -# - TRAVIS_COMMIT: The commit that the current build is testing. -# -# - TRAVIS_PULL_REQUEST: The pull request number if the current job is -# a pull request, “false” if it’s not a pull request. -# -# - TRAVIS_PULL_REQUEST_BRANCH: If the current job is a pull request, -# the name of the branch from which the PR originated. "" if the -# current job is a push build. - -echo $TRAVIS_PULL_REQUEST_BRANCH -echo $TRAVIS_PULL_REQUEST -echo $TRAVIS_BRANCH -echo $TRAVIS_COMMIT - -if [ $TRAVIS_PULL_REQUEST == "669" ] || [ $TRAVIS_BRANCH == "ssr-merge" ]; then - mathcomp_CI_BRANCH=ssr-merge - mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git -fi - -echo "DEBUG: ci-user-overlay.sh 0" -if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then - echo "DEBUG: ci-user-overlay.sh 1" - bedrock_src_CI_BRANCH=trunk__API - bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git - bedrock_facade_CI_BRANCH=trunk__API - bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git - fiat_parsers_CI_BRANCH=trunk__API - fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git -fi - -if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums" ]; then - math_classes_CI_BRANCH=external-bignums - math_classes_CI_GITURL=https://github.com/letouzey/math-classes.git - Corn_CI_BRANCH=external-bignums - Corn_CI_GITURL=https://github.com/letouzey/corn.git -fi - -if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins" ]; then - CompCert_CI_BRANCH=less_init_plugins - CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git - VST_CI_BRANCH=less_init_plugins - VST_CI_GITURL=https://github.com/letouzey/VST.git - fiat_crypto_CI_BRANCH=less_init_plugins - fiat_crypto_CI_GITURL=https://github.com/letouzey/fiat-crypto.git -fi diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh new file mode 100644 index 000000000..af4a96f4a --- /dev/null +++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then + mathcomp_CI_BRANCH=ssr-merge + mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md new file mode 100644 index 000000000..9146d3d52 --- /dev/null +++ b/dev/ci/user-overlays/README.md @@ -0,0 +1,14 @@ +# Add overlays for your pull requests in this directory + +An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh). + +The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`. + +Example: `00669-maximedenes-ssr-merge.sh` containing + +``` +if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then + mathcomp_CI_BRANCH=ssr-merge + mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git +fi +``` |