Zulip Chat Archive
Stream: PR reviews
Topic: documentation PRs
Scott Morrison (Oct 07 2018 at 10:58):
https://github.com/leanprover/mathlib/pull/400 and https://github.com/leanprover/mathlib/pull/395 are pure documentation, and can be merged.
Scott Morrison (Oct 07 2018 at 11:21):
... and have now been merged!
Last updated: Dec 20 2023 at 11:08 UTC