Closed MattTriano closed 1 year ago
I'm kind of confused about this. The PR already merged successfully (and I had pulled the updated main back into my local). I followed the given steps (below), I pulled the branch, I found there weren't any changed files (although there was a new commit; the merge commit). As I'm not that concerned with having an immaculate history, I'll probably add another commit to merge it again.
git pull origin main
git checkout parcel_assessment_dwh_dev
git merge main
<resolve merge commits>
git push -u origin parcel_assessment_dwh_dev
Well that's something. After executing git push -u origin parcel_assessment_dwh_dev
from my local repo, GitHub closed this out this PR (although it shows the PR was closed rather than merged, while it was definitely merged). Kind of irritating; I was ok with having an extra merge commit in the history, but that's easy for someone reading history to identify and understand. This situation, however, is bizarre and is a real speedbump when reading.
Closes #89