My bad, I missed the last digit of the bug report ID, so bot has not picked it up and I will have to do his job: Fixed in commit 3ca84dca.
My bad, I missed the last digit of the bug report ID, so bot has not picked it up and I will have to do his job: Fixed in commit 3ca84dca.