Edward, On Sun, Jul 26, 2020 at 6:52 AM Edward K. Ream <edream...@gmail.com> wrote: [...]
> P. S. I am alarmed by the potential loss of data when merging git branches. > > When I merged the "keys" branch into devel I mistakenly resolved a merge > conflict by taking devel's version of leoSettings.leo. That was just wrong. > > After deleting the "keys" branch, there seems to be no way recover the > lost key bindings. I would have thought that the git merge would have > preserved all previous changes to leoSettings.leo, but I was not able to > see those changes. Fortunately, the required change could easily be deduced. > [...] >From https://git-scm.com/book/en/v2/Git-Branching-Branches-in-a-Nutshell, "a branch in Git is simply a lightweight movable pointer to one of these commits". So when you delete a branch, you only lose the named pointer to the commit. Your merge commit shows which commit the keys branch used to point to: $ git log -n1 818de411e61 commit 818de411e6130086714a2f6bcb97ab52e6182674 Merge: *cc568d628* 060811435 Author: Edward K. Ream <edream...@gmail.com> Date: Sat Jul 25 08:43:33 2020 -0500 Merge devel into keys, using devel's leoSettings.leo Before you deleted the keys branch, it pointed to commit cc568d628 and you can see the changes to leo settings with this command: $ git log -p cc568d628 leo/config/leoSettings.leo No commits are lost when you delete a branch. A pull request from the keys branch into devel would have only helped you in that it would not have allowed you to merge into the devel branch due to the merge conflicts. You would have had to resolve the merge conflicts in the *keys* branch *before* merging into devel. There, one last round of testing might have exposed the issue, but maybe not. Or maybe inspecting the diffs one last time through the pull request UI might have helped you spot the issue. Either way, I don't think a PR provides any extra history preservation. The commits are all still there. Brian -- You received this message because you are subscribed to the Google Groups "leo-editor" group. To unsubscribe from this group and stop receiving emails from it, send an email to leo-editor+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/leo-editor/CAO5X8CxHkqZmfW6smQd60pv2HFxG-qP3cwZ%3D9RBCGs9XTprPFg%40mail.gmail.com.
