----- Op 11 jan 2021 om 18:29 schreef Stefan Monnier [email protected]: > > Similarly here, I don't see why a doubled up-arrow (I guess `⇑` ?) > would convey the semantics in a more intuitive manner than a `!`.
The doubled up-arrow that I meant is in the screenshot in attach. I am not sure however whether the Alto Serif Smalltalk-72 font, is a faithful reproduction of how old Xerox systems/old terminals looked like ...
