diff options
| author | Florian Angeletti <florian.angeletti@inria.fr> | 2023-03-06 16:41:44 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-03-06 16:41:44 +0100 |
| commit | db01922ef5e39e28b1256e5f8c37029216f220e6 (patch) | |
| tree | a197a36d932223409cc28d6876230a30ed5b1b06 /manual/src | |
| parent | b21919c1eb7e61c8e44f79f648fcacd394d0df4f (diff) | |
| parent | 5c95ef937799e4cf82ee9f6d37be3b00b21950d8 (diff) | |
| download | ocaml-db01922ef5e39e28b1256e5f8c37029216f220e6.tar.gz | |
Merge pull request #12076 from gasche/manual-pdf-target
Minor ergonomic improvements to the manual Makefile
Diffstat (limited to 'manual/src')
| -rw-r--r-- | manual/src/Makefile | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/manual/src/Makefile b/manual/src/Makefile index 5e2e7af08d..12849462c9 100644 --- a/manual/src/Makefile +++ b/manual/src/Makefile @@ -54,7 +54,7 @@ endif $(DIRS): $(MKDIR) $@ -manual: files latex_files | texstuff +pdf: files latex_files | texstuff cd texstuff \ && TEXINPUTS=$(TEXINPUTS) pdflatex manual.tex @@ -101,9 +101,9 @@ all: $(MAKE) html $(MAKE) text $(MAKE) info - $(MAKE) manual + $(MAKE) pdf $(MAKE) index - $(MAKE) manual + $(MAKE) pdf release: all cp htmlman/manual.html $(RELEASE)refman.html |