Skip to content

Conversation

mantepse
Copy link
Contributor

fix #40935 in posets

as with #40939: we have to decide whether this does not pollute the name space too much.

Copy link

Documentation preview for this PR (built with commit cd2aae5; changes) is ready! 🎉
This preview will update shortly after each push to this PR.

Copy link
Contributor

@fchapoton fchapoton left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ok, let's move on

@fchapoton
Copy link
Contributor

as a general comment, maybe one can think about deprecating all these aliases much later ?

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

Successfully merging this pull request may close these issues.

harmonize xxx_number
2 participants