[16:40:44] <wikibugs>	 10serviceops, 10MediaWiki-General, 10MediaWiki-Stakeholders-Group, 10Release-Engineering-Team, and 4 others: Drop official PHP 7.2 support in MediaWiki 1.35 - https://phabricator.wikimedia.org/T257879 (10Akuckartz) Can this be decided now?  I have reread the comments. I only found this one which is somehow...