This patch has been applied as 3e000955cd232c437cbe6994c124e30a35bc2605,
closing the bug.