Merge dev into master

Created by: dominikwerder

This pull request should get our github-based inter-site/group peer-review started. :-)

It is a pull request which combines several unfortunately unrelated changes which had been already merged into 'dev' into one bigger pull-request, but I think to get started, this may be better than no pull request at all for these changes.