Remove GitHub Workflow for mirroring to Gitlab

There was an advent recently, the Pipelines in Gitlab took a very long
time to execute, and used up my entire quota of free runners. At first
I thought of just adding timeouts, but then I thought there might be
better approaches to integrating with Gitlab.

So I'm removing the Gitlab integration for now, maybe in the future
when quotas are restored I'll set up a more convenient and thoughtful
integration again.

.github/workflows/gitlab.yml

@@ -1,23 +0,0 @@
-name: GitLab
-
-on:
-  push:
-  workflow_dispatch:
-
-jobs:
-  mirror:
-    name: Mirroring to GitLab
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          fetch-depth: 0
-      - uses: webfactory/ssh-agent@v0.9.0
-        with:
-          ssh-private-key: ${{ secrets.SSH_PRIVATE_KEY }}
-      - name: Mirror repository to Gitlab
-        run: |
-          set -e -x
-          ssh-keyscan -H "${{ vars.GITLAB_HOSTNAME }}" | tee -a ~/.ssh/known_hosts
-          git remote add gitlab "${{ vars.GITLAB_REPO_SSH }}"
-          git push --force gitlab "$GITHUB_REF_NAME"