Replying to @realn2s

@realn2s In order to get rid of the first of the
three commits in this PR, do a git rebase -i HEAD~3, delete the first commit and
git push -f to the branch.

Mon, 21 Oct 2019 20:11:56 UTC