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