This is to reconcile divergence in history between the Gitlab and Github repos due to a PR from the Github side.