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 _______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel