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