Display notification banners, for example on panic:

leanprover-community / lean4web

The Lean 4 web editor

https://live.lean-lang.org/

Apache License 2.0

68 stars 18 forks source link

Open joneugster opened 2 months ago

joneugster commented 2 months ago

#eval (panic "oh no" : Nat)

joneugster commented 2 months ago

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