diff options
| author | Pierre-Marie Pédrot | 2018-10-19 15:10:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-16 11:45:55 +0100 |
| commit | ad6d5a658806d1c0cf46a39f58113bfbd2ac808d (patch) | |
| tree | f57ac270631b9cd2ac00d22651902c6b2f0905e3 /dev | |
| parent | 778213b89d893b55e572fc1813c7209d647ed6b0 (diff) | |
Remove the implicit tactic feature following #7229.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/08779-ppedrot-rm-implicit-tactic.sh | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/08779-ppedrot-rm-implicit-tactic.sh b/dev/ci/user-overlays/08779-ppedrot-rm-implicit-tactic.sh new file mode 100644 index 0000000000..4536c62c64 --- /dev/null +++ b/dev/ci/user-overlays/08779-ppedrot-rm-implicit-tactic.sh @@ -0,0 +1,8 @@ +_OVERLAY_BRANCH=rm-implicit-tactic + +if [ "$CI_PULL_REQUEST" = "8779" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + ltac2_CI_REF="$_OVERLAY_BRANCH" + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + +fi |