Merge branch 'release/19.12'

This commit merges the release/19.12 branch excluding
commit 418924b6c3845f26734, which was meant for release/19.12 only.

It was created with:

git merge --no-commit release/19.12
git revert --no-commit 418924b6c3
git commit