changeset 67191 | 9ab34bb83a84 |
parent 67138 | 82283d52b4d6 |
child 67194 | 1c0a6a957114 |
--- a/etc/options Tue Dec 12 17:47:23 2017 +0100 +++ b/etc/options Tue Dec 12 17:46:22 2017 +0100 @@ -13,6 +13,8 @@ -- "alternative document variants (separated by colons)" option document_tags : string = "" -- "default command tags (separated by commas)" +option document_positions : bool = true + -- "inline original source positions into generated tex files" option thy_output_display : bool = false -- "indicate output as multi-line display-style material"