25 juni 2019 kl. 17.26 skrev Eli Zaretskii : > >> The question is whether it is too late to fix the bug, or if it needs to be documented. > > Both, I think ;-) Documenting a bug rather than fixing it never feels very satisfactory, but it may be the lesser evil. What about this patch?