בתאריך יום ו׳, 4 באוג׳ 2023, 13:53, מאת Brian Wolff bawolff@gmail.com:
Our understanding is that renaming extensions in MediaWiki is a long
and complicated process, so we'll likely not be able to rename it in the foreseeable future.
Why?
Renaming is usually a bad thing because it often confuses the hell out of users, but from a technical perspective it is pretty trivial.
--
I'm not the biggest expert on MediaWiki, but from the little I do know, the truth is closer to what Bawolff says. It's just a bit of careful searching and replacing. And in this case, it probably doesn't affect the users very much, because, as I've already written above, the name is not seen by most users in the frontend.
Although precisely because of that, it's not the most important thing to do either. It will just become a bit confusing in the long run that the ORES technology is declared as deprecated and the servers are turned off, but the ORES extension is still installed on some big wikis.
If this extension only adds the Recent Changes filtering and highlighting, perhaps it can be given a name that describes its function, such as "MLRevisionLabels" or something like that.