Hello Pavel,

> Could you please push it? I don't have such permissions.

I pushed the patch, after having made some minor editorial modifications
to the commit message and ChangeLog entry (added a period at the end of
the sentence describing the change).

Attached is what just got pushed.

-- 
Joel