diff options
| author | Arnaud Spiwack | 2016-07-30 17:13:27 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2016-11-07 19:49:24 +0100 |
| commit | 970bd8e901267916ae23bbe661d05c7d64f60b48 (patch) | |
| tree | 0b1b78b8580bb19af44fb62396820afa6ca03ec2 /doc/RecTutorial/RecTutorial.v | |
| parent | 0f5e89ec54bc613f59ce971e6a95ed1161ffc37b (diff) | |
Sort search results by relevance
This orders the results of search commands (such as `Search`,
`SearchAbout`, …) according to a "relevance" metric to minimise.
In this minimal version, the metric is the size of the displayed term.
Diffstat (limited to 'doc/RecTutorial/RecTutorial.v')
0 files changed, 0 insertions, 0 deletions