users-guide: Eliminate some redundant index entries
authorBen Gamari <ben@smart-cactus.org>
Mon, 24 Jul 2017 01:31:47 +0000 (21:31 -0400)
committerBen Gamari <ben@smart-cactus.org>
Mon, 24 Jul 2017 22:59:58 +0000 (18:59 -0400)
commit58b62d6b2bffcd31c0f3425330ff738f6ba37271
treebe93809691f1ecadb9b0fd540a649e635cb18db6
parent0c04d7873fc3825b86e44c52e36ab9baca02c959
users-guide: Eliminate some redundant index entries
docs/users_guide/profiling.rst