website 404

Stream: lean4

[Kevin Buzzard]

https://lean-lang.org/documentation/setup/ in the subsection "Setting up Lean" (near the bottom, I don't mean the main heading) the first line is "See also the quickstart instructions for a standard setup with VS Code as the editor" and the link on "quickstart" is to https://lean-lang.org/documentation/setup/quickstart.md which is a 404 for me.

[Kevin Buzzard]

Wait, I've now found https://docs.lean-lang.org/lean4/doc/setup.html too. Is the link in my first post supposed to even exist any more? I found the first link in https://lean-lang.org/documentation/ which I got to from the https://lean-lang.org/ home page.

[David Thrane Christiansen]

Sorry about that . I've just fixed these two links, and the build/deploy script is running. I'll post again when the fix is up.

[David Thrane Christiansen]

Deployed. Thanks again!