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

[Alissa Tung]

@Joachim Breitner

#announce rather than here?

Thank you, that makes sense. I took a quick look, and it seems moving the topic might require admin privileges :thinking: I am not sure

[Joachim Breitner]

Maybe some admin will move the first message to #announce, and maybe the rest of this thread to #general ?

[Alissa Tung]

Maybe some admin will move the first message to #announce, and maybe the rest of this thread to #general ?

Got it, sorry, I hope I didn't cause too much trouble