Commit 2023-04-24 23:44 26fdd3e3
View on Github →fix: enable ↦ in server mode (#3556)
Apparently we didn't enable the pp.unicode.fun in server mode, so you got inconsistent output depending on whether you run the lean file on the command-line (↦) or in the editor (=>). This change makes the options uniform.