Added by Kostas Papadimitriou over 8 years ago
Merge branch 'master' into packaging
Conflicts: .gitignore