Summary of changes: f4c14f4... dist-git conversion (*) e6c4c16... - Update to 1.17 (*) 89ff86c... Merge commit 'f4c14f430ff5c32d96c7dbff5c465d8b1a13099a' int 8687175... Merge branch 'master' into f13 (*) This commit already existed in another branch; no separate mail sent