GitHub Codespace can't find /etc/localtime

Stream: mathlib4

[Junyan Xu]

Codespace is unusable now with the error

/workspaces/mathlib4> lake serve -- /workspaces/mathlib4
Watchdog error: no such file or directory (error code: 2)
  file: /etc/localtime

everytime I tried to start the Lean server in a successfully configured codespace. I think it's likely due to some recent change in the codespace side, since I'm unable to find relevant recent from the Lean side.

[Bryan Gin-ge Chen]

The issue #31824 and associated PR #31826 look related. @Yakov Pechersky @Jon Eugster are either of you available to take a look?

[Yakov Pechersky]

It's not clear to me what changed about the lean process to require localtime, and also, it should be present in the ubuntu base image.