Reinhard Pointner dffcf5aa2b * rename 'development' Git branch to 'devel' (naming it HEAD is a bad idea)		2013-12-20 09:30:59 +00:00
..
sourceforge	* rename 'development' Git branch to 'devel' (naming it HEAD is a bad idea)	2013-12-20 09:30:59 +00:00