Yesterday, in response to a Pull Request, I did a Squash/Merge from a dev_branch to master.
When I look at the Pull Request (now closed), it shows the “Merged” tag and correctly lists the 10 commits (shows commit messages/ids) that went into the merge. As expected, the last one listed is the tip of dev_branch. When I select the link to that commit, it correctly shows that the last commit on dev_branch consisted exclusively of the deletion of 3 unused files.
When I go to the master branch, and examine the commit corresponding to the aforementioned merge/pull request, the comments show the appropriate/same 10 commit messages from the merge. But the list of files changed does not include the 3 that were deleted by the last commit on dev_branch. So, the files are still present on master.
There seems to be a mis-match between what happened with the Squash/Merge and what happened with the Pull.
Is this a bug in GitHub’s Pull/Merge functionality? Or am I missing something?