| Fri, 11 May 2018 20:22:20 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 11 May 2018 20:05:37 +0200 | wenzelm | clarified output: avoid costly operations on huge blobs; | changeset | files |
| Fri, 11 May 2018 19:59:05 +0200 | wenzelm | unused; | changeset | files |
| Fri, 11 May 2018 19:57:49 +0200 | wenzelm | more scalable -- avoid huge lines within stdout; | changeset | files |