* The '.php5' entrypoints were deprecated in I68b1ae842, $wgScriptExtension
in I3690f78bc.
* Drop the associated ResourceLoader configuration variable, too. `mwgrep`
shows no usage in the MediaWiki namespace.
* Keep the scriptExtension configuration parameter for FileRepo for people who
would like to interoperate with older MediaWiki installations that still use
'.php5'.
Change-Id: I17c8a15484b7e82cd5970d34e688109a2aae3840
