| Sun, 20 Dec 2015 13:06:26 +0100 | wenzelm | renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning; | changeset | files |
| Sun, 20 Dec 2015 13:03:41 +0100 | wenzelm | proper formatting via Pretty.string_of; | changeset | files |
| Sun, 20 Dec 2015 12:50:48 +0100 | wenzelm | unused; | changeset | files |