--- a/src/Doc/System/Presentation.thy Wed Nov 18 13:14:01 2020 +0100
+++ b/src/Doc/System/Presentation.thy Wed Nov 18 13:16:08 2020 +0100
@@ -130,6 +130,7 @@
Options are:
-O set option "document_output", relative to current directory
+ -P DIR enable HTML/PDF presentation in directory (":" for default)
-V verbose latex
-d DIR include session directory
-n no build of session
@@ -144,7 +145,8 @@
notably essential Isabelle style files, and \<^verbatim>\<open>session.tex\<close> to input all
theory sources from the session (excluding imports from other sessions).
- \<^medskip> Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-v\<close> have the same meaning as for @{tool build}.
+ \<^medskip> Options \<^verbatim>\<open>-P\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-v\<close> have the same meaning as for @{tool
+ build}.
\<^medskip> Option \<^verbatim>\<open>-V\<close> prints full output of {\LaTeX} tools.