diff options
| author | Maxime Dénès | 2019-05-13 11:40:03 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-13 11:40:24 +0200 |
| commit | 96f31931743c950f006682a398c501c30e96fda0 (patch) | |
| tree | 4fb0df42b96bc0bd42803a51e31ba043795140f0 /dev/ci | |
| parent | cf9f4e566b87d2875f757bb7d54ee4421988e315 (diff) | |
Add overlay for Unicoq
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh new file mode 100644 index 0000000000..bc8aa33565 --- /dev/null +++ b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then + + unicoq_CI_REF=detype-anonymous + unicoq_CI_GITURL=https://github.com/maximedenes/unicoq + +fi |