Fix pull request 640. For some reason github didn't allow a clean merge...

Fix pull request 640. For some reason github didn't allow a clean merge althought there weren't any conflicts. Fix it so that it's easier to just merge via the UI.