Re: [VOTE] Merge Knuth branch back into HEAD

[Jeremias Maerki]

Looks like we're ok for the merge. Shall I simply do it or does anyone
want to have a chance to commit his work before that? I'm not doing it
before I've fixed my current hardware problems anyway.

Jeremias Maerki