Closed CommanderStorm closed 8 months ago
I merge them most of the times with other PRs :) should we still switch to the TUM-Bot?
should we still switch to the TUM-Bot
Yes, but that requires asking @kordianbruck for the correct PAT for the bot (I don't have access to it ^^).
@jakobkoerber whenever I merge such a PR (only documentation), should I merge it or leave it to you?