Fix duplicate search results

We currently list the same page multiple times if,
for example, both the title and content search
match it. Since the preview is always the same,
this is not very helpful.

Author: wlach

sphinx/themes/basic/static/searchtools.js

@@ -362,12 +362,14 @@ const Search = {
 
     // remove duplicate search results
     // note the reversing of results, so that in the case of duplicates, the highest-scoring entry is kept
+    // this may remove some entries which refer to slightly different parts of the same document
+    // but this is a tradeoff to avoid showing the same document multiple times (the preview always looks the
+    // same, so this is not very useful)
     let seen = new Set();
     results = results.reverse().reduce((acc, result) => {
-      let resultStr = result.slice(0, 4).concat([result[5]]).map(v => String(v)).join(',');
-      if (!seen.has(resultStr)) {
+      if (!seen.has(result[0])) {
         acc.push(result);
-        seen.add(resultStr);
+        seen.add(result[0]);
       }
       return acc;
     }, []);