>FYI, this patch is obsolete as 0012b5d ("fix indentation and code style >for various Options grid") was pushed a bit over two hours ago. Oops, didn't see that one, sorry about that.