Feedback requested: dropping PHP 7.2 support for MediaWiki 1.35
https://phabricator.wikimedia.org/T257879 recommends dropping support for
PHP 7.2 in the upcoming MediaWiki 1.35 release. (It would still be
supported in master as it will probably take months for Wikimedia
production to switch.) Tl;dr: 1.35 is an LTS release which we'll support
for 3 years, and supporting an old PHP version in an LTS release tends to
be inconvenient in a number of ways. More details in the task.