Newsgroups: php.internals Path: news.php.net Xref: news.php.net php.internals:111129 Return-Path: Delivered-To: mailing list internals@lists.php.net Received: (qmail 47299 invoked from network); 22 Jul 2020 17:54:53 -0000 Received: from unknown (HELO localhost.localdomain) (76.75.200.58) by pb1.pair.com with SMTP; 22 Jul 2020 17:54:53 -0000 To: internals@lists.php.net References: Date: Wed, 22 Jul 2020 17:49:21 +0100 User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: en-GB Content-Transfer-Encoding: 7bit X-Posted-By: 87.81.129.66 Subject: Re: [PHP-DEV] The @@ is terrible, are we sure we're OK with it? From: marandall@php.net (Mark Randall) Message-ID: On 22/07/2020 17:43, Dik Takken wrote: > That means we effectively disregard the preferences of the ones who > voted for the @@ syntax. We do not know what the @@ voters would have > chosen if the choice was between << >> and #[]. In case the @@ voters > have a preference for << >> the result could turn out differently. The > only way to know is to take another vote. Yes we do - it was a ranked choice vote where voters selected their first, second and third preferences. If @@ is eliminated, the second choice of all those who voted for it as their first choice is already known. Mark Randall