Set up a mirror to dev

We need to set up a mirror to dev in order to have a backup registry. We mostly need this for versions

Create repo in dev https://dev.gitlab.org/gitlab/gitlab-docs
Set up mirror push
Make sure we use only variables in .gitlab-ci.yml (no path hard-coding) so that the different registry can be picked up https://gitlab.com/gitlab-com/gitlab-docs/merge_requests/242

Edited Apr 04, 2018 by Achilleas Pipinellis