web editor: unknown module prefix 'Mathlib'

Stream: general

[Eric Wieser]

In the web editor, the following

import Mathlib

gives

unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:

/lean/lib/lean

Batteries is similarly afflicted, unsurprisingly.

[Junyan Xu]

https://lean.math.hhu.de/ is okay, but https://live.lean-lang.org/ is broken

[Joachim Breitner]

Fixed