I just noticed that a bunch (~10) of code review appeared in gerrit that have long been merged. Example:
- CR in gerrit: https://gerrit.wikimedia.org/r/#/c/mediawiki/extensions/BlueSpiceFoundation/+/539616/ with commit hash de81ba25d91609f105ec7516879a8c2affb91831
- The same commit already merged into branch master https://github.com/wikimedia/mediawiki-extensions-BlueSpiceFoundation/commit/de81ba25d91609f105ec7516879a8c2affb91831 (here is an actual file in master that has been added by the change: https://github.com/wikimedia/mediawiki-extensions-BlueSpiceFoundation/blob/master/tests/phpunit/ExtensionAttributeBasedRegistryTest.php)
Could this be due to yesterday's gerrit server maintenance?
What should I do with these? Review/Merge them again? Abandon them? Delete them in another way?