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

From: João Távora <[email-masked]>
Date: Mon, 6 Nov 2023 16:20:52 +0000

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,
João