diff options
| author | Pierre-Marie Pédrot | 2018-05-25 10:57:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-25 10:57:55 +0200 |
| commit | 2e3fcd691a66683ea3d043c7c7bafbf1bcdfecf4 (patch) | |
| tree | 06a3e6ccd536d69c55d4cae95b5b55a80cbb01b1 /dev | |
| parent | 46df9a89b530fb076a13c177945323886cc6c575 (diff) | |
| parent | 1f4beb7369a0462502b26476e8748f21cc92ef72 (diff) | |
Merge PR #7196: [tactics] Remove anonymous fix/cofix form.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh new file mode 100644 index 0000000000..ea9cd8ee07 --- /dev/null +++ b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh @@ -0,0 +1,21 @@ +if [ "$CI_PULL_REQUEST" = "7196" ] || [ "$CI_BRANCH" = "tactics+push_fix_naming_out" ] || [ "$CI_BRANCH" = "pr-7196" ]; then + + # Needed overlays: https://gitlab.com/coq/coq/pipelines/21244550 + # + # equations + # ltac2 + + # The below developments should instead use a backwards compatible fix. + # + # color + # iris-lambda-rust + # math-classes + # formal-topology + + ltac2_CI_BRANCH=tactics+push_fix_naming_out + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=tactics+push_fix_naming_out + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi |