commit: e8a2786d6d4defa29f8991eb03e1dd975311e5ae

[log]
author: Eric Wieser <wieser.eric@gmail.com>

Tue Mar 26 09:00:25 2024 +0000
committer: GitHub <noreply@github.com>

Tue Mar 26 09:00:25 2024 +0000
tree: 053182fc8f329991d3c7b1baafec94f7ff9f1ac4
parent: 4c0106d757d4d6d3b7f3903611ce22100d539d2a [diff]

fix: actually catch the error code from MoveFileEx (#3753)

A user on Zulip [reported seeing an error code of "no
error"](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60lake.20update.60.20broken.20on.20Windows.20.28.3F.29/near/429134334)
here.

src/runtime/io.cpp[diff]

1 file changed

tree: 053182fc8f329991d3c7b1baafec94f7ff9f1ac4

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.