Merge branch 'dev'
We are now merging the reverted merge we did on the dev branch into the master. It's confusing.
Authored by: Jurgen J. Vinju 2014-12-04
Parent(s): [00a7fe][7a654b]
Child(ren): [3543d5][9ac30d]