I was reading some code today and I suddenly realized that Resources.php
in MediaWiki code is indeed a PHP file, instead of a JSON file, unlike
almost all ResourceLoader module definitions in almost all extensions.
Is there a reason for this, or is it simply because no one has changed
it yet? (It looks like it might be slightly tricky to change, because
the JSON definitions loading is tied to loading extensions…)
--
Bartosz Dziewoński