diff options
| author | Emilio Jesus Gallego Arias | 2020-03-22 00:30:25 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-22 00:30:25 -0400 |
| commit | ec4b889aa4e837bd82a7d0a059d0c967cde1ac46 (patch) | |
| tree | b0945180cd3501e463f1804e12d06a13aed1fa60 /Makefile.dune | |
| parent | 4d025d4161599ea20cd1dbf489a6412f019a7a7e (diff) | |
| parent | 80f3011eb5ca479b9b1f059c0f04e131028d5312 (diff) | |
Merge PR #11855: Build and install refman with Dune.
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Diffstat (limited to 'Makefile.dune')
| -rw-r--r-- | Makefile.dune | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/Makefile.dune b/Makefile.dune index 499ad0d16b..0520d43da9 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -4,7 +4,7 @@ .PHONY: help voboot states world watch check # Main developer targets .PHONY: coq coqide coqide-server # Package targets .PHONY: quickbyte quickopt quickide # Partial / quick developer targets -.PHONY: refman-html stdlib-html apidoc # Documentation targets +.PHONY: refman-html refman-pdf stdlib-html apidoc # Documentation targets .PHONY: test-suite release # Accessory targets .PHONY: fmt ocheck ireport clean # Maintenance targets @@ -32,6 +32,7 @@ help: @echo "" @echo " - test-suite: run Coq's test suite" @echo " - refman-html: build Coq's reference manual [HTML version]" + @echo " - refman-pdf: build Coq's reference manual [PDF version]" @echo " - stdlib-html: build Coq's Stdlib documentation [HTML version]" @echo " - apidoc: build ML API documentation" @echo " - release: build Coq in release mode" @@ -92,6 +93,9 @@ test-suite: voboot refman-html: voboot dune build @refman-html +refman-pdf: voboot + dune build @refman-pdf + stdlib-html: voboot dune build @stdlib-html |