| changeset 76440 | d7a3a0a793e2 |
| parent 76420 | 809cd1195795 |
| child 76451 | 87cd8506e000 |
--- a/src/Doc/Demo_LIPIcs/ROOT Fri Nov 04 18:59:54 2022 +0100 +++ b/src/Doc/Demo_LIPIcs/ROOT Fri Nov 04 19:57:21 2022 +0100 @@ -1,3 +1,5 @@ +chapter Doc + session Demo_LIPIcs (doc) = HOL + options [document_variants = "demo_lipics", document_build = "pdflatex", document_heading_prefix = "", document_comment_latex]