diff -r fd6dc1a4b9ca -r 1cbac4ae934d src/Doc/System/Presentation.thy
--- 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.