changeset 48527 | 4ee8d70cd5a3 |
parent 48520 | 6d4ea2efa64b |
child 48580 | 9df76dd45900 |
--- a/etc/options Thu Jul 26 19:40:19 2012 +0200 +++ b/etc/options Thu Jul 26 19:41:05 2012 +0200 @@ -27,6 +27,8 @@ declare names_short : bool = false declare names_unique : bool = true +declare pretty_margin : int = 76 + declare thy_output_display : bool = false declare thy_output_quotes : bool = false declare thy_output_indent : int = 0