diff options
| author | Gaëtan Gilbert | 2018-06-25 12:59:42 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-25 16:27:19 +0200 |
| commit | ca9e02ad1882cc4268ae1bcf0f573d24b92fa695 (patch) | |
| tree | ab2bdd8415bf2b2c627b2b345299989078e36419 /dev/ci | |
| parent | d389d88a7cec1b30b42c11d0dbff3f566b51e81a (diff) | |
Add overlay for Equations
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/07859-printers.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/07859-printers.sh b/dev/ci/user-overlays/07859-printers.sh new file mode 100644 index 0000000000..27f588e214 --- /dev/null +++ b/dev/ci/user-overlays/07859-printers.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "7859" ] || [ "$CI_BRANCH" = "rm-univ-broken-printing" ]; then + Equations_CI_BRANCH=fix-printers + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations +fi |