Merge tag 'v1.2'

When I prepared the 1.2 release, things probably happpened in the
following order:

    1. I created the preparation commits.

    2. I created an MR containing those commits.

    3. I merged the MR using Marge. Marge amended the commit messages
       with links to the MR.

    4. I tagged the last local commit.

    5. I pushed the tag.

In step 4 I should have reset my local checkout to the version on the
origin repo, which had diverged from my local version due to Marge's
commit message modifications. I didn't do that, so the master branch
ended up pointing to a different version than the tagged commit. This
merge commit makes the tagged commit part of the master branch.

0 files changed, 0 insertions, 0 deletions