Mirror this repository to the IN GitLab server

[MaxEtMoritz]

I guess most students have already used the IN GitLab for various projects and some students (including me) also (want to) use it for their bachelor thesis.
Since this repo is hosted on GitHub, keeping it up-to-date across systems would be a bit tedious (although this repository has not changed for a while now). It would be easier for students if this repository was mirrored to the IN GitLab instance so they can fork it from there directly.
Since the IN GitLab does not seem to allow pulling mirrors, you'd have to do a pushing mirror from GitHub.
Googling, i found the following GitHub action that does exactly that: https://github.com/marketplace/actions/mirroring-repository

unfortunately i don't have experience with GitHub actions (and my thesis is not yet ready so i have no time to try it).

A problem that may arise is Students wanting to commit to this repository via the IN GitLab. in theory you could set up the IN GitLab to mirror back to GitHub, but that would (with high probability) lead to an endless mirroring loop then 🔁