changeset 49542 | 4ee8d70cd5a3 |
parent 49535 | 6d4ea2efa64b |
child 49595 | 9df76dd45900 |
1.1 --- a/etc/options Thu Jul 26 19:40:19 2012 +0200 1.2 +++ b/etc/options Thu Jul 26 19:41:05 2012 +0200 1.3 @@ -27,6 +27,8 @@ 1.4 declare names_short : bool = false 1.5 declare names_unique : bool = true 1.6 1.7 +declare pretty_margin : int = 76 1.8 + 1.9 declare thy_output_display : bool = false 1.10 declare thy_output_quotes : bool = false 1.11 declare thy_output_indent : int = 0