diff options
| author | Maxime Dénès | 2018-03-09 17:16:53 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-09 17:16:53 +0100 |
| commit | 3b4bae6246b780961aa49b81a074e77189252bb3 (patch) | |
| tree | 1fe0006899d6e09f54b960e42c576f13747f5d77 /dev | |
| parent | 5542ffe43dde333cec6d118fd4b0424313330c33 (diff) | |
| parent | a8297dd69f840a23740e7b36f852522d7c3471f9 (diff) | |
Merge PR #6923: Export options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/06923-ppedrot-export-options.sh | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/06923-ppedrot-export-options.sh b/dev/ci/user-overlays/06923-ppedrot-export-options.sh new file mode 100644 index 0000000000..333a9e84bd --- /dev/null +++ b/dev/ci/user-overlays/06923-ppedrot-export-options.sh @@ -0,0 +1,7 @@ +if [ "$CI_PULL_REQUEST" = "6923" ] || [ "$CI_BRANCH" = "export-options" ]; then + ltac2_CI_BRANCH=export-options + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + + Equations_CI_BRANCH=export-options + Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations +fi |