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 -- PHP Internals - PHP Runtime Development Mailing List To unsubscribe, visit: https://www.php.net/unsub.php
