Skip to content

add almost 2 fully normal characterization to strongly collectionwise normal#1094

Merged
StevenClontz merged 2 commits into
mainfrom
StevenClontz/almost2fullynormal
Dec 16, 2024
Merged

add almost 2 fully normal characterization to strongly collectionwise normal#1094
StevenClontz merged 2 commits into
mainfrom
StevenClontz/almost2fullynormal

Conversation

@StevenClontz
Copy link
Copy Markdown
Member

@Moniker1998
Copy link
Copy Markdown
Collaborator

Moniker1998 commented Dec 16, 2024

@StevenClontz I've clarified what it means to be an almost 2-star refinement. Do you agree with the changes?

@StevenClontz
Copy link
Copy Markdown
Member Author

Thanks for the fixes @Moniker1998!

@StevenClontz
Copy link
Copy Markdown
Member Author

And thanks for the approving review @Moniker1998 as well. In the future, you're welcome to use the "Squash and Merge" button to wrap up any approved pull request that requires no further discussion.

@StevenClontz StevenClontz merged commit b7a8912 into main Dec 16, 2024
@StevenClontz StevenClontz deleted the StevenClontz/almost2fullynormal branch December 16, 2024 12:41
@prabau
Copy link
Copy Markdown
Collaborator

prabau commented Dec 16, 2024

@Moniker1998
FYI, when you do a "squash and merge", it is recommended to first blank out the associated description before clicking on "squash and merge". I.e., only keep the title.

For an explanation, see
#912 (comment) and the following comment (and by the way, Steven is now kind of ok with doing this, right?)
and #779 (comment).

@StevenClontz
Copy link
Copy Markdown
Member Author

and by the way, Steven is now kind of ok with doing this, right?

I'm still not 100% sold on the utility of it (and this week I'm hacking on a project where we don't do that step, so I'm getting confused on which workflow I'm using lol) but I've started doing it here. We can discuss at a future meeting.

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.

4 participants