changeset 77554 | 4465d9dff448 |
parent 76556 | c7f3e94fce7b |
child 82032 | 9bc4f982aef4 |
--- a/src/Doc/System/Presentation.thy Tue Mar 07 10:16:24 2023 +0100 +++ b/src/Doc/System/Presentation.thy Tue Mar 07 10:57:50 2023 +0100 @@ -22,7 +22,7 @@ with the PDF into the given directory (relative to the session directory). Alternatively, @{tool_ref document} may be used to turn the generated - {\LaTeX} sources of a session (exports from its build database) into PDF. + {\LaTeX} sources of a session (exports from its session build database) into PDF. \<close>