Subject: Re: bug#48841: bug#47711: bug#48841: bug#47711: [PATCH VERSION 2] Add new `completion-filter-completions` API and deferred highlighting

From: Dmitry Gutov <[email-masked]>
Date: Mon, 6 Nov 2023 21:38:55 +0200

On 06/11/2023 18:20, João Távora wrote:
> On Wed, Nov 1, 2023 at 10:45 PM Dmitry Gutov<[email-masked]>  wrote:
> 
>> I guess we should wait a few days to see if anyone has more comments,
>> and then install this?
> Five days elapsed, and no more comments came in, so I addressed your
> comments and Eli's and I pushed this to master as
> dfffb91a70532ac0021648ba692336331cbe0499.

Thanks!

And thanks to Daniel for the original proposal and design work.