aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-09-01 11:51:41 +0200
committerPierre-Marie Pédrot2020-09-01 11:51:41 +0200
commit0d30f79268fea18ef99c040a859956f61c3d978a (patch)
tree26694ab196e67dde80cc8489236770bda59a061c /dev
parent46768229c5349aa92a8107cd0a6ded32fd22d768 (diff)
parent576c1153dae2b3660d35127862aeb3d528eb6d8d (diff)
Merge PR #12892: Update update_global_env usage
Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: ppedrot
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh9
1 files changed, 9 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh b/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh
new file mode 100644
index 0000000000..f0878202d3
--- /dev/null
+++ b/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "12892" ] || [ "$CI_BRANCH" = "update-s-univs" ]; then
+
+ elpi_CI_REF=update-s-univs
+ elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+ equations_CI_REF=update-s-univs
+ equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+fi