Closed kba closed 4 years ago
Currently, I'm the only one working on the upstream repository and all previous developers know of this repo. I always push to both.
I'll look into making the source repository public again. It was already public, but was transferred from a user account to a group. Gitlab doesn't seem to allow making a repository public without making the whole group public, which I have to discuss with the other chair members. I'll leave this bug open until then.
Ok, the gitlab group and the repository there is now public. I also set up automatic mirroring in gitlab (which only seems to allow pushing in our instance), so the Github repo will always be up to date.
As our gitlab instance only creates accounts for members of the university and accounts for external people have to be requested, I disabled gitlab issues and will use the issues here exclusively. I updated the description on github accordingly.
Otherwise it is impossible to know whether this is up-to-date. If issues are found, should they be raised here? Are the upstream maintainers aware of this repo?