-
- Downloads
Change the default print names for the characters #\^\\, #\^], #\^^,
and #\^_ to be the ASCII names. (This is for consistency. There was a bug in printing the name for #\^\\, and this works around that.)
Loading
Please register or sign in to comment