leanprover-community.github.io icon indicating copy to clipboard operation
leanprover-community.github.io copied to clipboard
verified publisher icon leanprover-community

Naming conventions doc has significant amount of duplicated text

Open spl opened this issue 7 years ago • 1 comments

docs/naming.md has entire sections of nearly duplicate text. Just search for “Sometimes” and you'll find it.

spl avatar Apr 29 '18 09:04 spl

The new location is https://github.com/leanprover-community/leanprover-community.github.io/blob/3a6244b3b59d42a02316ef23ea7d7f646aebe491/templates/contribute/naming.md

bryangingechen avatar Jun 14 '20 17:06 bryangingechen