Added by Kostas Papadimitriou about 10 years ago
Merge branch 'hotfix-0.14.2' into debian-hotfix-0.14.2
Conflicts: version