IGBF-1846

Sorry for the hassle! The old commit is still in the pull request. See these instructions on how to amend a git commit message without leaving the old one in the project history: https://help.github.com/en/articles/changing-a-commit-message It's a bit risky, and is never something you should do if anyone else has cloned your repository and is working on the branch you are trying to revise. But, in this case, it is fine. Or, if you feel a bit worried about it (and I would not blame you one bit if yes!) you can create a new branch, cherry-pick the commits from your old one, and before you commit, edit the commit message. All this probably seems like a huge pain, but it really helps me -- and everyone else! -- to have the git commit messages follow a very clear pattern. It helps a lot when reading dozens and dozens of these to try to follow the history of a project.