-
Notifications
You must be signed in to change notification settings - Fork 256
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(MetricSpace/HausdorffDistance): split in two #9809
Conversation
Adjusted imports, so should build. Needs main module docstrings.
8ac1725
to
bf679b2
Compare
Can you explain what the two new files contain in the PR description? |
Merged master, and extended the PR description. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it makes more sense to move the thickening material to Topology.MetricSpace.Thickening
. It's not really a subset of Hausdorff distance material.
@YaelDillies Makes sense, I have moved the files as you suggested. (Despite the force-push, only the last three commits are new.) |
bfd3a64
to
888a360
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
maintainer merge
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks!
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
Thank you for the review. |
The file was becoming a bit large (1550 lines). Split in two files of about 900 and 700 lines: the first file contains more basic material, the second file contains all material related to thickenings. Extend the module docstrings by mentioning the main results in this file.
Pull request successfully merged into master. Build succeeded: |
The file was becoming a bit large (1550 lines). Split in two files of about 900 and 700 lines: the first file contains more basic material, the second file contains all material related to thickenings. Extend the module docstrings by mentioning the main results in this file.
The file was becoming a bit large (1550 lines). Split in two files of about 900 and 700 lines:
the first file contains more basic material, the second file contains all material related to thickenings.
Extend the module docstrings by mentioning the main results in this file.
Feedback about the new docstrings is welcome; I wrote them from scratch.