etc/options
changeset 67194 1c0a6a957114
parent 67191 9ab34bb83a84
child 67273 c573cfb2c407
     1.1 --- a/etc/options	Tue Dec 12 18:53:40 2017 +0100
     1.2 +++ b/etc/options	Wed Dec 13 16:18:40 2017 +0100
     1.3 @@ -13,8 +13,6 @@
     1.4    -- "alternative document variants (separated by colons)"
     1.5  option document_tags : string = ""
     1.6    -- "default command tags (separated by commas)"
     1.7 -option document_positions : bool = true
     1.8 -  -- "inline original source positions into generated tex files"
     1.9  
    1.10  option thy_output_display : bool = false
    1.11    -- "indicate output as multi-line display-style material"