redo of commit b292a5d0f274d26b2a9ed4c31a222cdd7bd3d71a
Jonathan fixed this on the gui-merging branch, however then it was
merged into master without it.