Merge branch 'dev' of https://opensourceprojects.eu/git/p/ossmeter/code-0 into dev
Authored by: Jurgen J. Vinju 2014-06-18
Parent(s): [838ada][c0d617]
Child(ren): [8dd9c6][a8e5bd]