Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Rename Marginf to MarginF32 for consistency with CornerRadiusF32 #5677

Merged
merged 3 commits into from
Feb 11, 2025
Merged

Rename Marginf to MarginF32 for consistency with CornerRadiusF32 #5677

merged 3 commits into from
Feb 11, 2025

Conversation

lucasmerlin
Copy link
Collaborator

  • I have followed the instructions in the PR template

@github-actions GitHub Actions
Copy link

github-actions bot commented Feb 4, 2025

Preview available at https://egui-pr-preview.github.io/pr/5677-marginf32
Note that it might take a couple seconds for the update to show up after the preview_build workflow has completed.

emilk
emilk requested changes Feb 4, 2025
View reviewed changes
Copy link
Owner

@emilk emilk left a comment

Choose a reason for hiding this comment

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

Since we forgot to merge this before the release (oops!) we'll have to also add

#[deprecated = "Renamed to MarginF32"]
pub type Marginf = MarginF32;

and export that

@emilk
Copy link
Owner

emilk commented Feb 4, 2025

Let's also add "Make sure there are no important unmerged PRs" to the release checklist 😆

@emilk emilk merged commit 510b3cd into master Feb 11, 2025
46 of 47 checks passed
@emilk emilk deleted the margin_f32 branch February 11, 2025 10:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@emilk emilk emilk requested changes

Assignees
No one assigned
Labels
dev-experience
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@lucasmerlin @emilk