aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-10-11 14:55:11 +0200
committerGaëtan Gilbert2018-11-02 13:26:16 +0100
commitc73c1ed2315ec01f2f2963b9a40cdf45c5907139 (patch)
treed0abea261313254055d71000194693c122b7f68f /dev
parent0a478031f0213ef74c3649ea1a8d58aa89e54416 (diff)
Add overlays (command driven attributes)
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/user-overlays/08515-command-atts.sh12
1 files changed, 12 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/08515-command-atts.sh b/dev/ci/user-overlays/08515-command-atts.sh
new file mode 100755
index 0000000000..4605255d5e
--- /dev/null
+++ b/dev/ci/user-overlays/08515-command-atts.sh
@@ -0,0 +1,12 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8515" ] || [ "$CI_BRANCH" = "command-atts" ]; then
+ ltac2_CI_REF=command-atts
+ ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2
+
+ Equations_CI_REF=command-atts
+ Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+ plugin_tutorial_CI_REF=command-atts
+ plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials
+fi