Web version error: /project/mathlib-demo.lean not found

Stream: general

[Thomas Murrills]

Just reporting a small web version error I'm seeing: if you write

import Mathlib

then the last position in the file has the error

no such file or directory (error code: 2)
  file: /project/mathlib-demo.lean

Can anyone reproduce?

[Kim Morrison]

This is likely the issue discussed at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/reading.20the.20.22visible.22.20file.2C.20rather.20than.20the.20saved.20one/near/454337536, with a fix in the merge queue now.