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.

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

[maint] add soname to library #63

Merged
merged 1 commit into from
Aug 19, 2020
Merged

Conversation

tylerjw
Copy link
Member

@tylerjw tylerjw commented Aug 19, 2020

soname added to library for Noetic releases

@tylerjw tylerjw requested a review from v4hn August 19, 2020 17:31
Copy link
Contributor

@v4hn v4hn left a comment

Choose a reason for hiding this comment

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

LGTM

@davetcoleman davetcoleman merged commit 4ccc89e into moveit:noetic-devel Aug 19, 2020
@rhaschke
Copy link
Contributor

@davetcoleman, we should discuss (and agree on a common strategy) whether or not to keep tags like [maint] in the commit message when merging. So far, we didn't.

@v4hn
Copy link
Contributor

v4hn commented Aug 20, 2020 via email

@davetcoleman
Copy link
Member

Yea I don't think we need to over-dictate how people write their commit messages. Though I do like the "WIP" standard as we have a bot that enforces PRs from not being merged until its removed.

@rhaschke
Copy link
Contributor

My key point was that I am fine with tags in github PR titles, but I would like to remove those tags when actually merging.

@tylerjw
Copy link
Member Author

tylerjw commented Aug 20, 2020

I put this tag in because I just did the cleanup for changelists. It would be nice if these tags were in the commit message than the changelist generator would get them and it'd remove a manual step when generating a changelist (not that it is that bad).

@rhaschke
Copy link
Contributor

IMO the tags clutter the git commit history. I see your motivation of avoiding the manual work for changelogs. But there, we need to format and cleanup manually anyway.

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.

None yet

4 participants