Fix a bad merge

There was a bad interaction between
commits 6777f54fa44341dd4b23456c97d97c6e4ffe915f
and 23e47f5621271db9b84f53f15a3e3d81d8b8b48d.

Change-Id: Ic408f8b4859d83d89c612748ee6e772b57830d96
1 file changed