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

[João Távora]

On Wed, Nov 1, 2023 at 10:45 PM Dmitry Gutov <dmitry@gutov.dev> 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