Merge contribution guides?

Stream: lean4

[Denis Gorbachev]

Currently, there are two guides:

• CONTRIBUTING.md
• doc/contributions.md

Usages:

• The CONTRIBUTING.md is supposed to be the main guide (as recommended by GitHub).
• The doc/contributions.md is mentioned in the PULL_REQUEST_TEMPLATE.md

Would it be better to merge the guides into a single CONTRIBUTING.md, and link to that file from PULL_REQUEST_TEMPLATE.md?

[Denis Gorbachev]

@Mac Malone Should I open a PR that merges the guides?

[Scott Morrison]

Thank you, this would be helpful. Where there are disagreements, doc/constributions.md is correct.

[Eric Wieser]

I assume the doc/ one was intended to feature on the html webpage?

[Denis Gorbachev]

Opened https://github.com/leanprover/lean4/pull/2624