aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/user-overlays/12611-ejgallego-record+refactor.sh9
-rw-r--r--dev/doc/build-system.dune.md6
2 files changed, 15 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
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 8b0bf216e3..de3d5a3d15 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -175,6 +175,12 @@ local copy of Coq. For this purpose, Dune supports the `-p` option, so
version of Coq libs, and use a "release" profile that for example
enables stronger compiler optimizations.
+## OPAM file generation
+
+`.opam` files are automatically generated by Dune from the package
+descriptions in the `dune-project` file; see Dune's manual for more
+details.
+
## Stanzas
`dune` files contain the so-called "stanzas", that may declare: