Hi all,
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.
Your feedback in the task would be appreciated, especially if you would be
affected by the change in a positive or negative way.