deleted posts (trashcan)

Stream: general

[Yaël Dillies]

Ever since the dawn of time (dated back to the advent of Lean 4), I have been using doc-gen to build my documentation and then mv .lake/build/doc website/docs to make it appear on my project website. However, this broke at some between the 7th and 17th of December.

[Henrik Böving]

That is incorrect, mathlib4_docs builds like this since the dawn of time and still builds as such

[Yaël Dillies]

Sorry, it is very confusing why it broke now rather than earlier, but LeanCamCombi docs weren't being built anymore because we commented out the instructions