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.