diff options
| author | Emilio Jesus Gallego Arias | 2019-02-25 09:27:58 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-26 21:49:13 +0100 |
| commit | 07ce2588740f689fe92a8d00dd1aeccda5255130 (patch) | |
| tree | 234671fa7f181f9d4f8205a6de1da3ca3c35e83a /Makefile.dune | |
| parent | 9d6f268723b6352a97bcc3baf0df57f1c1b251fa (diff) | |
[dune] Simple rule to generate Stdlib's documentation.
Ideally this will be handled by Dune's native library support, but
this could be useful for the likes of #9648.
I am not sure what should be done w.r.t. style files.
Diffstat (limited to 'Makefile.dune')
| -rw-r--r-- | Makefile.dune | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/Makefile.dune b/Makefile.dune index 29f6fed974..da4c59af75 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -4,7 +4,8 @@ .PHONY: help voboot states world watch check # Main developer targets .PHONY: coq coqide coqide-server # Package targets .PHONY: quickbyte quickopt # Partial / quick developer targets -.PHONY: test-suite refman-html apidoc release # Accesory targets +.PHONY: refman-html stdlib-html apidoc # Documentation targets +.PHONY: test-suite release # Accesory targets .PHONY: ocheck trunk ireport clean # Maintenance targets # use DUNEOPT=--display=short for a more verbose build @@ -29,6 +30,7 @@ help: @echo "" @echo " - test-suite: run Coq's test suite" @echo " - refman-html: build Coq's reference manual [HTML version]" + @echo " - stdlib-html: build Coq's Stdlib documentation [HTML version]" @echo " - apidoc: build ML API documentation" @echo " - release: build Coq in release mode" @echo "" @@ -81,6 +83,9 @@ test-suite: voboot refman-html: voboot dune build @refman-html +stdlib-html: voboot + dune build @stdlib-html + apidoc: voboot dune build $(DUNEOPT) @doc |