21:16:05 PHP Notice: Undefined index: R in /opt/phpunit-patch-coverage/vendor/mediawiki/phpunit-patch-coverage/src/Git.php on line 57 21:16:05 PHP Fatal error: Uncaught Error: Cannot access empty property in /opt/phpunit-patch-coverage/vendor/mediawiki/phpunit-patch-coverage/src/Git.php:59 21:16:05 Stack trace: 21:16:05 #0 /opt/phpunit-patch-coverage/vendor/mediawiki/phpunit-patch-coverage/src/CheckCommand.php(161): MediaWiki\Tool\PatchCoverage\Git->getChangedFiles('9f86db20286c2c3...') 21:16:05 #1 /opt/phpunit-patch-coverage/vendor/symfony/console/Command/Command.php(251): MediaWiki\Tool\PatchCoverage\CheckCommand->execute(Object(Symfony\Component\Console\Input\ArgvInput), Object(Symfony\Component\Console\Output\ConsoleOutput)) 21:16:05 #2 /opt/phpunit-patch-coverage/vendor/symfony/console/Application.php(946): Symfony\Component\Console\Command\Command->run(Object(Symfony\Component\Console\Input\ArgvInput), Object(Symfony\Component\Console\Output\ConsoleOutput)) 21:16:05 #3 /opt/phpunit-patch-coverage/vendor/symfony/console/Application.php(248): Symfony\Component\Console\Application->doRunCommand(Object(MediaWiki\Tool\PatchCoverage\CheckCommand), Object(Symfony\Component\Console\Input\ArgvInput), Object(Symfo in /opt/phpunit-patch-coverage/vendor/mediawiki/phpunit-patch-coverage/src/Git.php on line 59
https://integration.wikimedia.org/ci/job/mediawiki-phpunit-coverage-patch-docker/792/console
Looks like I didn't think about file renames when implementing https://gerrit.wikimedia.org/r/plugins/gitiles/mediawiki/tools/phpunit-patch-coverage/+/master/src/Git.php#28
Probably it would be easiest to consider renames as deletion of one file and creation of another.