Skip to content

Console menu: don't print special characters when output is not tty#5155

Merged
kit-ty-kate merged 2 commits intoocaml:masterfrom rjbou:menuJul 29, 2022