Show part of the document ID for the pages found

Review Request #129364 - Created Nov. 9, 2016 and submitted

Information
Luigi Toscano
khelpcenter
master
Reviewers
docs
pino
Extract the relevant part of the document ID (without the name of the page) and show it before the name. The result of the man page indexer already follows this pattern.

Compiles, the short name is shown in the search results.

Burkhard Lück
Burkhard Lück
Luigi Toscano
Review request changed

Status: Closed (submitted)

Change Summary:

Submitted with commit 5c9ffc89f39b855432d3e6872d51d6ced0ca2bff by Luigi Toscano to branch master.
Loading...