Yes, here is the PR I sent from my openamp branch: https://github.com/apache/incubator-nuttx/pull/894 But merged by you two hour ago. Do you select "Create a merge commit" or "Rebase and merge"?
I always select rebase and merge, but it is hard to construct what happened in the past from the present. But, in any case, I would not have merged onto an openamp branch because I don't have one: "Merge branch 'master' of github.com:apache/incubator-nuttx into openamp"
In any case, it looks we are okay other than some duplicate commits. So that was my primary concern.
