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: May 02 2025 at 03:31 UTC