Zulip Chat Archive

Stream: general

Topic: Criterion for inclusion in Reservoir

Yaël Dillies (Dec 12 2023 at 20:02):

How does #reservoir know what repositories to include? In particular I was surprised to see https://github.com/YaelDillies/LeanAPAP is missing.

Yaël Dillies (Dec 12 2023 at 20:02):

(can we have the linkifier pretty please? :smile:)

Bryan Gin-ge Chen (Dec 12 2023 at 20:36):

Tada: #reservoir

Patrick Massot (Dec 12 2023 at 20:45):

@Yaël Dillies see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/How.20to.20tag.20a.20repository/near/403416211

Yaël Dillies (Dec 12 2023 at 20:58):

Ahah, I knew it was discussed somewhere but couldn't find it!

Last updated: Dec 20 2023 at 11:08 UTC