Closed thorimur closed 7 months ago
This is very minor, but thought I'd mention that the color status to the left of the line number seems to be off by one:
import Lean elab "#wait" : command => IO.sleep 10000 -- yellow appears here #wait
Link to live code; noticed on Firefox and Safari.
(Also thanks for lean4web; it's extremely useful! :) )
This is very minor, but thought I'd mention that the color status to the left of the line number seems to be off by one:
Link to live code; noticed on Firefox and Safari.
(Also thanks for lean4web; it's extremely useful! :) )