ci: remove Github mirroring

Gitlab now has built-in mirroring, so we don't need to have a CI
step for this now.

.gitlab-ci.yml

@@ -11,26 +11,6 @@ variables:
   IGNORE_HOSTKEY: "ssh -o StrictHostKeyChecking=no -o UserKnownHostsFile=/dev/null"
 
 
-mirror repository:
-    stage: build
-    only:
-        - branches@kwant/kwant
-    allow_failure: true
-    variables:
-      REPOS: "git@github.com:kwant-project/kwant.git git@gitlab.com:kwant/kwant.git"
-    before_script:
-      - HOSTS=$(for REPO in $REPOS; do echo ${REPO%:*} | cut -d'@' -f2; done)
-      - mkdir ~/.ssh && chmod 700 ~/.ssh
-      - for HOST in $HOSTS; do ssh-keyscan $HOST >> ~/.ssh/known_hosts; done
-      - echo "$DEPLOY_KEY" > ~/.ssh/id_rsa && chmod 600 ~/.ssh/id_rsa
-    after_script:
-      - rm -rf ~/.ssh
-    script:
-      - ORIGIN_URL=$(git config --get remote.origin.url)
-      - cd $(mktemp -d); git clone --bare $ORIGIN_URL .
-      - for REPO in $REPOS; do git push --mirror $REPO; done
-
-
 build package:
   stage: build
   script: