Added by Stavros Sachtouris almost 11 years ago
Merge branch 'release-0.10' into debian-release-0.10