aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rwxr-xr-xdev/ci/ci-basic-overlay.sh2
-rwxr-xr-xdev/ci/ci-sf.sh9
-rw-r--r--dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh15
3 files changed, 18 insertions, 8 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 50d4d21637..f422030b53 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -238,7 +238,7 @@
########################################################################
# plugin_tutorial
########################################################################
-: "${plugin_tutorial_CI_REF:=master}"
+: "${plugin_tutorial_CI_REF:=14b2976cdf67db788b79d9421ce1e89bd15c7313}"
: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}"
: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 58bbb7229f..60436e672c 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -8,11 +8,6 @@ wget -qO- "${sf_lf_CI_TARURL}" | tar xvz
wget -qO- "${sf_plf_CI_TARURL}" | tar xvz
wget -qO- "${sf_vfa_CI_TARURL}" | tar xvz
-sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v
-sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v
-
-( cd lf && make clean && make )
-
-( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make )
-
+( cd lf && make clean && make )
+( cd plf && make clean && make )
( cd vfa && make clean && make )
diff --git a/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh
new file mode 100644
index 0000000000..b3a9f67e00
--- /dev/null
+++ b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "8704" ] || [ "$CI_BRANCH" = "vernac+monify_hook" ]; then
+
+ # ltac2_CI_REF=rm-section-path
+ # ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+ plugin_tutorial_CI_REF=vernac+monify_hook
+ plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials
+
+ Elpi_CI_REF=vernac+monify_hook
+ Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+ Equations_CI_REF=vernac+monify_hook
+ Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi