lean4web icon indicating copy to clipboard operation
lean4web copied to clipboard
verified publisher icon leanprover-community

Display notification banners, for example on panic:

Open joneugster opened this issue 1 year ago • 1 comments 

#eval (panic "oh no" : Nat)

joneugster avatar Aug 11 '24 22:08 joneugster

With 72a64823d8a085fcac00decffcdde21bdb3f71ba, these errors appear in the browser console, but not yet as notification toast.

joneugster avatar Aug 13 '24 09:08 joneugster