Hi Clint,

On Tue, Oct 18, 2016 at 12:59:01PM +0000, Clint Adams wrote:
> Did you make a commit and forget to push?

Indeed. I rebased my unpublished local commit and pushed it now. Thank
you for the poke.

Helmut

Reply via email to