I reported an issue in opam-grep due to a line overflowing a character. Apparently it only happens with some fonts, but when this is the case, emojis like 'checkmark' can use two characters instead of one, leading to the estimation of the terminal width to be incorrect.
More precisely, as long as progress is happening and characters such as ⠼️ are being displayed, everything is fine, but when it finishes and a checkmark is displayed instead, it occupies 2 spaces and so the last character is displayed in the next line.
I don't know if something can be done about it, or if there's not much that can be done other than perhaps mentioning it somewhere in the documentation.
I reported an issue in opam-grep due to a line overflowing a character. Apparently it only happens with some fonts, but when this is the case, emojis like 'checkmark' can use two characters instead of one, leading to the estimation of the terminal width to be incorrect.
More precisely, as long as progress is happening and characters such as
⠼️are being displayed, everything is fine, but when it finishes and a checkmark is displayed instead, it occupies 2 spaces and so the last character is displayed in the next line.I don't know if something can be done about it, or if there's not much that can be done other than perhaps mentioning it somewhere in the documentation.