Hi!
Have there been any recent changes on the way Gerrit repos are mirrored to github? A few hour ago (as far as I can tell) the master branch of https://github.com/wikimedia/mediawiki-extensions-BlueSpiceSmartList has changed significantly. It was reset to a 7 year old version.
I believe this may be connected to the fact, that on Gerrit there seem to be two versions of that repo, with different casing:
- https://gerrit.wikimedia.org/r/plugins/gitiles/mediawiki/extensions/BlueSpiceSmartlist/ -> Lower case l, 7 year old master branch
- https://gerrit.wikimedia.org/r/plugins/gitiles/mediawiki/extensions/BlueSpiceSmartList/ -> Upper case L, 9 days old master branch
Unfortunately, I don't know why this is the case.
To me this seems to be the most likely cause of the behavior on github.com, as unlike Gerrit, it has case insensitive repo names.
Can you please help me figure out how to fix that? You can also delete the outdated repo, if that helps.