am 7ebafd5a: Merge change 9009 into donut

Merge commit '7ebafd5aa03e9d84696be0448f9d248e8f90e16c'

* commit '7ebafd5aa03e9d84696be0448f9d248e8f90e16c':
  Reapply modifications from 3175 to fix display of navTree in doc output.