Thanks, pushed to master. (Small wish: Please format the git commit comment according to conventions: One short (less than 79 characters) first line that summarizes the commit, followed if necessary by a blank line and one or several paragraphs, with max 79 character line length.) --tml