Closed silasary closed 7 years ago
Just hit merge and it'll work :)
Basically, this PR tries to merge into master. When you merged #12, you moved master forward. But it's still master, and now, if you merge my PR in, it'll go on top of the new front of master, rather than where it was when I opened the PR.
In other words, git knows what it's doing, and you don't need to worry about it :)
ah, thanks a lot for the explanation! where I work we also do version control development, but it is kind of "old fashioned" in the sense that this exact issue would mean that your #13 as it is would overwrite the changes I sent in #12.
I will now press "merge" with not only confidence but also a greater understanding :-)
(note: I will also update README to include the new optional flag in the input line to request the sideboard)
is there an easy way to commit these changes into the latest merge I did from #12 ?