Closed davetcoleman closed 9 years ago
@gavanderhoorn you should be able to merge this yourself now. thanks for helping!
np. Do you guys have a preference for merging using the Merge pull request button, or are command line merges ok as well?
Also, we have a rule that you should never merge your own PRs or commit directly to a repo's main branches. At least one person should always review any change.
That's ok: we got the same rules for ROS-Industrial repositories.
np. Do you guys have a preference for merging using the Merge pull request button, or are command line merges ok as well?
I've never done a command line merge and am not sure the difference in results. Does github still play nicely? I might have seen the result of a command line merge once in a different project and found it confusing.
Also, I'm not sure the correct way to write your name... would Gavander Hoorn be better?
np. Do you guys have a preference for merging using the Merge pull request button, or are command line merges ok as well?
I've never done a command line merge and am not sure the difference in results. Does github still play nicely? I might have seen the result of a command line merge once in a different project and found it confusing.
It shouldn't really matter. I don't really have a preference, but just thought I'd ask.
Also, I'm not sure the correct way to write your name... would Gavander Hoorn be better?
No, you got it right the first time ('G.A.' are the initials, the rest is prefix + surname).
@gavanderhoorn you should be able to merge this yourself now. thanks for helping!
Also, we have a rule that you should never merge your own PRs or commit directly to a repo's main branches. At least one person should always review any change.