Re: GitHub merge

2018-07-27 Thread Rob
Thanks, Terry and Jacob. Rob... On Friday, July 27, 2018 at 9:54:55 AM UTC-4, Terry Brown wrote: > > Based on looking at `gitk --all` and then perhaps more efficiently `git > log --stat`, I'd say what you did had no negative impact beyond perhaps an > unnecessary merge commit - i.e. it didn't

Re: GitHub merge

2018-07-27 Thread Terry Brown
Based on looking at `gitk --all` and then perhaps more efficiently `git log --stat`, I'd say what you did had no negative impact beyond perhaps an unnecessary merge commit - i.e. it didn't actually change any files in devel or anywhere else. Cheers -Terry On Fri, Jul 27, 2018 at 8:04 AM Rob

Re: GitHub merge

2018-07-27 Thread Terry Brown
It is in the main GitHub repo., but I'm not sure if it's doing any harm. I.e. it might just be merge commit that merges branches that were already in sync. bar trivial changes. I'll investigate a bit more. Cheers -Terry On Fri, Jul 27, 2018 at 8:04 AM Rob wrote: > After returning from an

GitHub merge

2018-07-27 Thread Rob
After returning from an extended trip last night, I tried syncing my local machine to the latest leo devel branch. I use GitHub Desktop on Win10. On my end, it appears that I may have unintentionally merged branches. See screenshot: