WIP: Merge dist2dist branch?
Can we please agree whether or not there is content in the dist2dist branch that is worth merging? The branch is WAY behind the master and I would like to clean up a little. Do you have any comments?
Aufgrund einer Konfigurationsänderung in GitLab wurden neue Nutzende, die sich zum ersten Mal zwischen dem 4.11.2025 und dem 13.01.2026 angemeldet haben, mit einem falschen Benutzernamen erstellt. Es wird dringend empfohlen, dass diese Nutzenden ihren Benutzernamen unter https://git.rwth-aachen.de/-/profile/account ändern. Eine Anleitung finden Sie hier: https://docs.gitlab.com/user/profile/#change-your-username. // Due to a configuration change in GitLab, new users who registered for the first time between November 4, 2025, and January 13, 2026, were created with an incorrect username. It is strongly recommended that these users change their username at https://git.rwth-aachen.de/-/profile/account. Instructions can be found here: https://docs.gitlab.com/user/profile/#change-your-username
Can we please agree whether or not there is content in the dist2dist branch that is worth merging? The branch is WAY behind the master and I would like to clean up a little. Do you have any comments?