Sat, 13 Jul 2013 14:11:48 +0200 | wenzelm | clarified some default options; | changeset | files |
Sat, 13 Jul 2013 13:58:13 +0200 | wenzelm | gutter icon for information messages; | changeset | files |
Sat, 13 Jul 2013 13:25:42 +0200 | wenzelm | more explicit Markup.information for messages produced by "auto" tools; | changeset | files |