Merge branch 'stable-3.0'

No-op merge, only to clear it. Originally caused by the unwanted merge
of commit c4576e9, which happened to be an ill-based repeat of commit
025de68. That led to the merge commit 4074ae3, base of this very merge.

The clean version of this merge was commit 00351af.

Change-Id: I07be4eae5af4dac008c7c1da1898707959be1391