# HG changeset patch # User wenzelm # Date 961969582 -7200 # Node ID 25245986e6670dada1100222bcbd12613f0ac51c # Parent 04a46ceace350176acc6fa7f145eec955d80f665 fbrk: 2 if not taken; diff -r 04a46ceace35 -r 25245986e667 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Sun Jun 25 23:46:03 2000 +0200 +++ b/src/Pure/General/pretty.ML Sun Jun 25 23:46:22 2000 +0200 @@ -147,7 +147,7 @@ val str = String o apsnd Real.round o Symbol.output_width; fun brk wd = Break (false, wd); -val fbrk = Break (true, 0); +val fbrk = Break (true, 2); fun blk (indent, es) = let