etc/options
changeset 48520 6d4ea2efa64b
parent 48516 c5d0f19ef7cb
child 48527 4ee8d70cd5a3
     1.1 --- a/etc/options	Thu Jul 26 17:16:02 2012 +0200
     1.2 +++ b/etc/options	Thu Jul 26 17:17:53 2012 +0200
     1.3 @@ -27,5 +27,11 @@
     1.4  declare names_short : bool = false
     1.5  declare names_unique : bool = true
     1.6  
     1.7 +declare thy_output_display : bool = false
     1.8 +declare thy_output_quotes : bool = false
     1.9 +declare thy_output_indent : int = 0
    1.10 +declare thy_output_source : bool = false
    1.11 +declare thy_output_break : bool = false
    1.12 +
    1.13  declare timing : bool = false
    1.14