Hello Dscho, Am 08.01.2018 um 21:45 schrieb Johannes Schindelin: > Isn't this identical to > https://public-inbox.org/git/20180103184852.27271-1-ava...@gmail.com/ ?
yes, indeed, thanks. So here's an upvote for Ævar's patch then. :) (I should have sent it earlier, but was not fully convinced it could be triggered in the wild.) René
