[02:49:50] <wikibugs>	 (03CR) 10jenkins-bot: build: Updating mediawiki/phan-taint-check-plugin to 1.5.0 [extensions/JADE] - 10https://gerrit.wikimedia.org/r/458983 (owner: 10Libraryupgrader)
[04:35:59] <wikibugs>	 (03CR) 10jenkins-bot: build: Updating mediawiki/phan-taint-check-plugin to 1.5.0 [extensions/ORES] - 10https://gerrit.wikimedia.org/r/459021 (owner: 10Libraryupgrader)
[21:35:35] <wikibugs>	 (03CR) 10MarcoAurelio: "Is this the real ORES repo or just some GitHub mirror from where deploys happen? IIRC some ORES/AI repos do host their code at GitHub and " [extensions/ORES] - 10https://gerrit.wikimedia.org/r/458872 (owner: 10Umherirrender)
[21:36:40] <wikibugs>	 (03CR) 10MarcoAurelio: "recheck" [extensions/ORES] - 10https://gerrit.wikimedia.org/r/458173 (owner: 10Acamicamacaraca)
[21:37:24] <Hauskatze>	 with regards to the bot comments above, can somebody help me, please?
[21:37:43] <Hauskatze>	 is extensions/ORES code really hosted on Gerrit or is this just another GitHub mirror?
[21:38:17] <wikibugs>	 (03CR) 10jerkins-bot: [V: 04-1] Add special page alias for Serbian [extensions/ORES] - 10https://gerrit.wikimedia.org/r/458173 (owner: 10Acamicamacaraca)
[21:39:22] <wikibugs>	 (03PS4) 10MarcoAurelio: Add special page alias for Serbian [extensions/ORES] - 10https://gerrit.wikimedia.org/r/458173 (owner: 10Acamicamacaraca)
[21:39:36] <wikibugs>	 (03PS5) 10MarcoAurelio: Add special page alias for Serbian [extensions/ORES] - 10https://gerrit.wikimedia.org/r/458173 (owner: 10Acamicamacaraca)
[21:40:05] <wikibugs>	 (03CR) 10MarcoAurelio: "PS3=rebase; PS4=adds the missing empty line at the EOTF." [extensions/ORES] - 10https://gerrit.wikimedia.org/r/458173 (owner: 10Acamicamacaraca)
[21:40:07] <wikibugs>	 (03CR) 10Umherirrender: "That are projects like scoring/ores, not the php code for the extension itself" [extensions/ORES] - 10https://gerrit.wikimedia.org/r/458872 (owner: 10Umherirrender)
[21:59:57] <wikibugs>	 (03CR) 10MarcoAurelio: [C: 032] Run stylelint also for less files [extensions/ORES] - 10https://gerrit.wikimedia.org/r/458872 (owner: 10Umherirrender)
[22:12:47] <wikibugs>	 (03Merged) 10jenkins-bot: Run stylelint also for less files [extensions/ORES] - 10https://gerrit.wikimedia.org/r/458872 (owner: 10Umherirrender)
[22:26:05] <wikibugs>	 (03CR) 10jenkins-bot: Run stylelint also for less files [extensions/ORES] - 10https://gerrit.wikimedia.org/r/458872 (owner: 10Umherirrender)