Zulip Chat Archive

Stream: PR reviews

Topic: Lean 3

Martin Dvořák (Dec 21 2022 at 08:12):

I think that pages about Lean 3 should explicitly say they are about Lean 3.
https://github.com/leanprover-community/leanprover-community.github.io/pull/301
https://github.com/leanprover-community/leanprover-community.github.io/pull/299

Martin Dvořák (Dec 21 2022 at 08:15):

https://github.com/leanprover-community/leanprover-community.github.io/pull/302

Martin Dvořák (Dec 21 2022 at 08:25):

https://github.com/leanprover-community/leanprover-community.github.io/pull/303

Patrick Massot (Dec 21 2022 at 08:47):

This is nice but why creating 4 PRs instead of one??

Martin Dvořák (Dec 21 2022 at 08:49):

Cuz I'm a dumb bitch.

Last updated: Dec 20 2023 at 11:08 UTC