Merge dev into master

This merges dev.gitlab.org master into CE master. This is necessary as a security MR (https://dev.gitlab.org/gitlab/gitlab-ee/merge_requests/826/) was merged into the stable branches as part of the last security release, but was not yet into master.