Am 23.04.18 um 14:18 schrieb Carl Eugen Hoyos: > 2018-04-22 23:16 GMT+02:00, Thilo Borgmann <thilo.borgmann at mail.de>: > > Why is this a separate patch? To make the git-work a bit easier - do you want it to be merged into the others, would it be sufficient to do that before pushing? -Thilo