Zulip Chat Archive
Stream: new members
Topic: Where to put the Lean Blueprint
Kyle Trinh (Nov 21 2024 at 18:30):
Hello, I am new here. I just want to check if the lean blueprint should be in the same repo as a Lean project as opposed to a separate repo. Thanks!
Bjørn Kjos-Hanssen (Nov 21 2024 at 18:43):
Yes, the same. Here's a working example.
Kyle Trinh (Nov 22 2024 at 01:11):
Thank you!
Last updated: May 02 2025 at 03:31 UTC