am 08b75cc3: Merge "misc header changes for r10d"

* commit '08b75cc3b7ccec1b2eb7d78d5bb49049490f3a37':
  misc header changes for r10d