etc/options
changeset 70121 61e26527480e
parent 69968 1a400b14fd3a
child 70122 a0b21b4b7a4a
     1.1 --- a/etc/options	Thu Apr 11 14:22:52 2019 +0200
     1.2 +++ b/etc/options	Thu Apr 11 15:44:06 2019 +0200
     1.3 @@ -18,8 +18,10 @@
     1.4    -- "indicate output as multi-line display-style material"
     1.5  option thy_output_break : bool = false
     1.6    -- "control line breaks in non-display material"
     1.7 +option thy_output_cartouche : bool = false
     1.8 +  -- "indicate if the output should be delimited as cartouche"
     1.9  option thy_output_quotes : bool = false
    1.10 -  -- "indicate if the output should be enclosed in double quotes"
    1.11 +  -- "indicate if the output should be delimited via double quotes"
    1.12  option thy_output_margin : int = 76
    1.13    -- "right margin / page width for printing of display material"
    1.14  option thy_output_indent : int = 0