diff options
| author | Pierre-Marie Pédrot | 2018-10-19 15:58:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:30:23 +0100 |
| commit | 58926ede84b84b2fb51e3d159872e1aaad339bf7 (patch) | |
| tree | a24c9535a55ef727bfedf69b2a55a4d0c370dd7c /dev | |
| parent | 733cb74a2038ff92156b7209713fc2ea741ccca6 (diff) | |
Adding overlays.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh new file mode 100644 index 0000000000..b05d02c5be --- /dev/null +++ b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh @@ -0,0 +1,14 @@ +_OVERLAY_BRANCH=clean-transp-state + +if [ "$CI_PULL_REQUEST" = "7925" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + unicoq_CI_REF="$_OVERLAY_BRANCH" + unicoq_CI_GITURL=https://github.com/ppedrot/unicoq + + equations_CI_REF="$_OVERLAY_BRANCH" + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + mtac2_CI_REF="$_OVERLAY_BRANCH" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + +fi |