diff options
| author | Pierre-Marie Pédrot | 2018-11-03 16:27:59 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-03 16:27:59 +0100 |
| commit | 10e2f279d97b15939e6bdc7658dee20e09b06653 (patch) | |
| tree | e04f05e6ee1efe1abae01ccccb96ecc5e3646088 /dev | |
| parent | 228066a783a581ba2b304a12d9fe5e8decebcc48 (diff) | |
| parent | d6619dda80e30adb3d8699c896374657a32ca4e6 (diff) | |
Merge PR #8844: Move abstract out of tactics.ml
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/08844-split-tactics.sh | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/08844-split-tactics.sh b/dev/ci/user-overlays/08844-split-tactics.sh new file mode 100644 index 0000000000..8ad8cba243 --- /dev/null +++ b/dev/ci/user-overlays/08844-split-tactics.sh @@ -0,0 +1,12 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8844" ] || [ "$CI_BRANCH" = "split-tactics" ]; then + Equations_CI_REF=split-tactics + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + ltac2_CI_REF=split-tactics + ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 + + fiat_parsers_CI_REF=split-tactics + fiat_parsers_CI_GITURL=https://github.com/SkySkimmer/fiat +fi |