From 593e99514abc1b43a011f4ae64f40443714b0a68 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 30 Jun 2020 18:03:14 +0200
Subject: [record] [ci] Overlay for elpi

We re-expose `declare_projections` and `declare_structure_entry` as it
is needed by coq-elpi.

Ideally we would provide a better way in recordops to interact with
this, in fact `declare_structure_entry` is just a wrapper around
recordops + libobject structure so there is hope it goes away entirely
in the future.

The need for Elpi to manually call `declare_projections` should
actually disappear in future refactorings.
---
 dev/ci/user-overlays/12611-ejgallego-record+refactor.sh | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 dev/ci/user-overlays/12611-ejgallego-record+refactor.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh b/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh
new file mode 100644
index 0000000000..b7d21ed59c
--- /dev/null
+++ b/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "12611" ] || [ "$CI_BRANCH" = "record+refactor" ]; then
+
+    elpi_CI_REF=record+refactor
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+#    mtac2_CI_REF=record+refactor
+#    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+fi
-- 
cgit v1.2.3