diff options
| author | Emilio Jesus Gallego Arias | 2020-06-30 18:03:14 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-13 19:12:29 +0100 |
| commit | 593e99514abc1b43a011f4ae64f40443714b0a68 (patch) | |
| tree | a7c9b1f2fdd4a45d8e11c980be79a23618a8e73a /dev/ci | |
| parent | df19ab7cc9931580171ed910f6b2d15ff8247492 (diff) | |
[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.
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/user-overlays/12611-ejgallego-record+refactor.sh | 9 |
1 files changed, 9 insertions, 0 deletions
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 |