diff options
| author | Enrico Tassi | 2019-06-11 19:32:44 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-11 21:05:06 +0200 |
| commit | c80a4599dfe5f3049323dd1aedf38e3072525d4f (patch) | |
| tree | 5b3b66521b6536c64aedc86936198969cded6505 | |
| parent | a93b3d8c630328ae6de0463fa6e4fa5d1a946dde (diff) | |
overlay
| -rw-r--r-- | dev/ci/user-overlays/10358-gares-elpi13.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/10358-gares-elpi13.sh b/dev/ci/user-overlays/10358-gares-elpi13.sh new file mode 100644 index 0000000000..d2ba9b5ddf --- /dev/null +++ b/dev/ci/user-overlays/10358-gares-elpi13.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10358" ] || [ "$CI_BRANCH" = "elpi-13-coq" ]; then + + elpi_CI_REF="elpi-13-coq" + elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi + +fi |