Taken from Jakob's merge of master: I should have applied his.

But the previous commit and this one include his changes (I think).