[rtems commit] Merge branch 'master' of ssh://dispatch.rtems.org/data/git/ rtems

[Chris Johns]

On 25/01/2016 08:51, Joel Sherrill wrote:
>
>     Joel, I think git log should contain the message so it might pay to
>     check what you have before you push.
>
>
> I am not sure what would be in the log in this situation that I would be
> looking for.
>

The merge message? I did not think a push merged anything so it must be 
present before you push.

Chris