| Sat, 08 May 2010 19:53:11 +0200 | wenzelm | discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally; | file | diff | annotate |
| Sat, 08 May 2010 19:14:13 +0200 | wenzelm | unified/simplified Pretty.margin_default; | file | diff | annotate |