aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dune
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-05-24 03:52:06 +0200
committerEmilio Jesus Gallego Arias2018-09-10 10:45:15 +0200
commit42bb3db8c897c5b3c82fcf1d4e4f71ee0e0d2bef (patch)
tree0851ea50e178b12dd1caacbd2ce20ad9cb58572d /Makefile.dune
parent73c3c7c6b3d35439c58126d0b55cf7a7e3235191 (diff)
[dune] Add apidoc target using `odoc`
We build the `@doc` target in the `dune` job: - The documentation can be found in `_build/default/_doc/` - We had to fix a couple of quoting problems.
Diffstat (limited to 'Makefile.dune')
-rw-r--r--Makefile.dune7
1 files changed, 7 insertions, 0 deletions
diff --git a/Makefile.dune b/Makefile.dune
index f90f555557..e04982650f 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -13,6 +13,7 @@ help:
@echo " - states: build a minimal functional coqtop"
@echo " - world: build all binaries and libraries"
@echo " - release: build Coq in release mode"
+ @echo " - apidoc: build ML API documentation"
@echo " - clean: remove build directory and autogenerated files"
@echo " - help: show this message"
@@ -29,6 +30,12 @@ world: voboot
release: voboot
dune build $(DUNEOPT) -p coq
+apidoc:
+ # Ugly workaround for https://github.com/ocaml/odoc/issues/148
+ mv checker/dune checker/dune.disabled || true
+ dune build $(DUNEOPT) @doc
+ mv checker/dune.disabled checker/dune || true
+
clean:
dune clean