-
Notifications
You must be signed in to change notification settings - Fork 68
Merge pull request #835 into branch v1.10 #552
Conversation
|
This one doesn't include the AUTHORS change. Can you add that commit to this PR? Some pro / Github tips:
|
|
Done. My name was added into "AUTHORS". |
|
I'm now a little confused by this PR -- it seems to have 2 duplicate commits (albeit one with a change to AUTHORS) and a merge commit...? Can you make this PR be just a cherry pick of the individual relevant commits from master? |
|
I combined the comments into one. I suppose this is all right. Please recheck it. |
|
@Zhiming-Wang Yes, this is better, thanks! In the future, note that you don't have to squash down to one commit. Can you still commit the change to AUTHORS to master (in a separate PR)? We like to see stuff on master before we approve putting them to the release branches. |
|
@jsquyres , Is it the master of open-mpi/ompi ? |
|
👍 |
Merge pull request #835 into branch v1.10
Convert csh script distscript.csh into a POSIX sh script
I merged the change set of "Pull Request" #835 into branch v1.10