diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-11 08:33:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-11 08:33:37 +0200 |
| commit | 357c94b3e42d4422e311799771f9e28249fc3608 (patch) | |
| tree | b9cbefb89a1e27d1f90edd378995f2527d3db054 | |
| parent | 306b45f889f83846b1ab10d3b37d9f3e7817a5db (diff) | |
Adding an overlay for Ltac2.
| -rw-r--r-- | dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh new file mode 100644 index 000000000..517088a24 --- /dev/null +++ b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then + + ltac2_CI_BRANCH=fast-constr-match-no-context + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + +fi |