Added by Stavros Sachtouris about 11 years ago
Merge branches 'develop' and 'debian-develop' into debian-develop