diff options
| author | Matthieu Sozeau | 2018-06-05 12:00:40 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-06-05 12:00:40 +0200 |
| commit | 56be411d5c582d6f644129dabda7ba036a4419a7 (patch) | |
| tree | def26fef6fc8b864253040206a099b14c5823703 /dev | |
| parent | f6538f1a7f8ad2bdc0bc446d4ca35078d55d63ee (diff) | |
| parent | 3490e3c0b7bbd574228725f8132082c519d0f1a2 (diff) | |
Merge PR #7495: Fix restrict_universe_context
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/07495-gares-elpi-test-bug.sh | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh new file mode 100644 index 0000000000..6939ead2ba --- /dev/null +++ b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh @@ -0,0 +1,8 @@ +if [ "$CI_PULL_REQUEST" = "7495" ] || [ "$CI_BRANCH" = "fix-restrict" ]; then + + # this branch contains a commit not present on coq-master that triggers + # the universe restriction bug #7472 + Elpi_CI_BRANCH=overlay-7495 + Elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi.git + +fi |