| Wed, 11 Oct 2017 21:36:53 +0200 | wenzelm | reactivated unfinished tool (cf. a3a847c4fbdb); | changeset | files |
| Wed, 11 Oct 2017 20:57:12 +0200 | wenzelm | tuned whitespace; | changeset | files |
| Wed, 11 Oct 2017 20:55:11 +0200 | wenzelm | clarified meta_digest; | changeset | files |
| Wed, 11 Oct 2017 20:46:38 +0200 | wenzelm | tuned; | changeset | files |