Commit 85eea96a3159c41b6630fd26d6f090484a131460

Stefano Lattarini 2011-01-11T02:35:38

Merge branch 'maint' Conflicts: ChangeLog Apparently I messed up doing a previous 'git pull', so that the "latest" maint I've merged into master (and pushed!) wasn't a fast-forward from origin/maint. Yay for me. This merge should help cleaning up the mess.