Alexandros,

Pushed as eb642f3d247ee0c74122017354c57bdce028eb57, with the 
indentation tweaks below (C-M-q in emacs, and moving the comment 
in-line).

Thanks!

T G-R