diff options
| author | Gaëtan Gilbert | 2018-10-30 13:34:06 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-30 15:45:12 +0100 |
| commit | d6619dda80e30adb3d8699c896374657a32ca4e6 (patch) | |
| tree | c5d86ae5b98e18d88b63b13ca3b4a6e741710554 /dev | |
| parent | 82105f030e13aebcb232eb912526ff8ca0650a24 (diff) | |
Overlays (#8844 split-tactics)
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 |