I pushed this as commit 3d2e41adf2. Thank you for the patch! -- Ricardo