Skip to content

box product of reals is not W but has points Gdelta#779

Merged
Almanzoris merged 5 commits into
mainfrom
StevenClontz/S107-W
Sep 22, 2024
Merged

box product of reals is not W but has points Gdelta#779
Almanzoris merged 5 commits into
mainfrom
StevenClontz/S107-W

Conversation

@StevenClontz
Copy link
Copy Markdown
Member

No description provided.

@StevenClontz StevenClontz marked this pull request as ready for review September 21, 2024 17:52
@Almanzoris
Copy link
Copy Markdown
Collaborator

I would say that I find it ready.

@StevenClontz
Copy link
Copy Markdown
Member Author

I would say that I find it ready.

Great! Then leave an approving review and click "squash and merge" to accept this contribution. Thanks for your review.

@Almanzoris Almanzoris merged commit d61c7eb into main Sep 22, 2024
@Almanzoris Almanzoris deleted the StevenClontz/S107-W branch September 22, 2024 13:57
@prabau
Copy link
Copy Markdown
Collaborator

prabau commented Sep 22, 2024

@Almanzoris FYI, about the meaning of "squash and merge". When working on a PR there are usually multiple commits. The "squash" part then squashes all these commits into a single combined commit, which is the one that gets merged into the main branch. Most of the time, the details of the individual commits do not matter. That's why when I do the "squash and merge" I usually blank out the list of individual commits in the description field before pressing the button. That way, one gets a cleaner log when doing git log on the command line, a lot easier to scan all the merged PRs. Something like this:

image

If you don't blank out the description, one ends up with something like this:

image

It's completely irrelevant that there was an intermediate commit that fixed indentation or another one with "small fixes" or ... or for my PR at the bottom another commit that fixed a typo. All that makes the overall list harder to scan. Not everybody agrees (@StevenClontz ?), but my recommendation would be to only keep the relevant overall title for the PR.

And note that if anybody cares, the details of the individual commits is still available on the github page for each PR.

@Almanzoris
Copy link
Copy Markdown
Collaborator

Yeah, you are right. My bad, and thank you for letting me know. I will keep this in mind for the next times.

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