Skip to content

Conversation

@tobiasgrosser
Copy link

Read this section before submitting

  • Ensure your PR follows the External Contribution Guidelines.
  • Please make sure the PR has excellent documentation and tests. If we label it missing documentation or missing tests then it needs fixing!
  • Include the link to your RFC or bug issue in the description.
  • If the issue does not already have approval from a developer, submit the PR as draft.
  • The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
  • A toolchain of the form leanprover/lean4-pr-releases:pr-release-NNNN for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing release-ci on its own line.
  • If you rebase your PR onto nightly-with-mathlib then CI will test Mathlib against your PR.
  • You can manage the awaiting-review, awaiting-author, and WIP labels yourself, by writing a comment containing one of these labels on its own line.
  • Remove this section, up to and including the --- before submitting.

Closes #0000 (RFC or bug issue number fixed by this PR, if any)

@tobiasgrosser
Copy link
Author

This has been merged months ago.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants