| Tue, 16 May 2017 16:04:50 +0200 | wenzelm | proper init_settings, before inspecting ML_HOME etc; | file | diff | annotate |
| Thu, 20 Oct 2016 11:04:38 +0200 | wenzelm | proper echo; | file | diff | annotate |
| Tue, 18 Oct 2016 16:03:30 +0200 | wenzelm | clarified modules; | file | diff | annotate |
| Thu, 13 Oct 2016 23:09:26 +0200 | wenzelm | tuned; | file | diff | annotate |
| Thu, 13 Oct 2016 15:17:10 +0200 | wenzelm | tuned signature; | file | diff | annotate |
| Thu, 13 Oct 2016 12:13:43 +0200 | wenzelm | clarified modules; | file | diff | annotate |