diff --git a/scripts/Makefile.alectryon b/scripts/Makefile.alectryon index 9b3fbb0f9ae43557c47844d11b1d19db66723029..2a02691b5f10ebada9859bcd524967e323f13699 100644 --- a/scripts/Makefile.alectryon +++ b/scripts/Makefile.alectryon @@ -9,3 +9,8 @@ tutorial: $(VOFILES) doc/tutorial.v $(SHOW)'Compiling the tutorial with alectryon: doc/tutorial.v -> html/tutorial.html' $(HIDE)mkdir -p html $(HIDE)alectryon -R . prosa --frontend coq+rst --backend webpage --output-directory "html" doc/tutorial.v + +tutorial-pdf: $(VOFILES) doc/tutorial.v + $(SHOW)'Compiling the tutorial with alectryon: doc/tutorial.v -> doc/tutorial.pdf' + $(HIDE)alectryon -R . prosa --frontend coq+rst --backend latex --output-directory "doc" doc/tutorial.v + $(HIDE)cd doc && pdflatex tutorial.tex