Just wanted to bring pull request #977 to attention since it got recently updated. It basically already got improved almost a year ago, and the last outstanding thing was a squash of two commits and a rebase. This is done now. It would be great it that PR could be merged soon. Thanks, Eberhard https://github.com/mono/mono/pull/977