Line-specific error

Stream: general

[Yaël Dillies]

You remember that incredible bug where a specific line was getting an error? Well, it seems like I'm onto another one. On line 282, around column 14, I get an unexpected end of string, whatever the code here actually is.
Unfortunately, I can't reproduce it. Restarting the Lean server made it go away.

[Shing Tak Lam]

lean#468 ?

[Yaël Dillies]

Oh yeah, sounds like it!