equal
deleted
inserted
replaced
7 |
7 |
8 option document : string = "" |
8 option document : string = "" |
9 -- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")" |
9 -- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")" |
10 option document_output : string = "" |
10 option document_output : string = "" |
11 -- "document output directory" |
11 -- "document output directory" |
|
12 option document_echo : bool = false |
|
13 -- "inform about document file names during session presentation" |
12 option document_variants : string = "document" |
14 option document_variants : string = "document" |
13 -- "alternative document variants (separated by colons)" |
15 -- "alternative document variants (separated by colons)" |
14 option document_tags : string = "" |
16 option document_tags : string = "" |
15 -- "default command tags (separated by commas)" |
17 -- "default command tags (separated by commas)" |
16 option document_bibliography : bool = false |
18 option document_bibliography : bool = false |