This makes it easier to automatically generate parts of the manager
documentation in the future.

Update #3993.