etc/options
changeset 48520 6d4ea2efa64b
parent 48516 c5d0f19ef7cb
child 48527 4ee8d70cd5a3
equal deleted inserted replaced
48519:5deda0549f97 48520:6d4ea2efa64b
    25 
    25 
    26 declare names_long : bool = false
    26 declare names_long : bool = false
    27 declare names_short : bool = false
    27 declare names_short : bool = false
    28 declare names_unique : bool = true
    28 declare names_unique : bool = true
    29 
    29 
       
    30 declare thy_output_display : bool = false
       
    31 declare thy_output_quotes : bool = false
       
    32 declare thy_output_indent : int = 0
       
    33 declare thy_output_source : bool = false
       
    34 declare thy_output_break : bool = false
       
    35 
    30 declare timing : bool = false
    36 declare timing : bool = false
    31 
    37