On Fri, Mar 27, 2020 at 11:07 AM Gavin Smith <[email protected]> wrote: > I will certainly add it but could you explain what difference it > makes? Does this fix the "font boosting" issue? > (https://lists.gnu.org/archive/html/bug-texinfo/2019-06/msg00000.html)
Done in commit 2509d615c.
