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.
  • 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

Closing as a very old PR.

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.

3 participants