Patch pushed as 9d21858e92afb3c7308953b33f8df1642f313a6f. Thanks. I added "François J " as copyright line, tell me if you want to modify it.