Merge pull request #616 from lean-ja/Seasawher/issue578

検索で見出し語が一番上に出てこないことがある
lean-ja · Aug 12, 2024 · 722d7c0 · 722d7c0
2 parents 94f8dc3 + 703576a
commit 722d7c0
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
@@ -20,7 +20,8 @@
         "mhutchie.git-graph",
         "Tyriar.sort-lines",
         "yzhang.markdown-all-in-one",
-        "PKief.material-icon-theme"
+        "PKief.material-icon-theme",
+        "juggernautjp.less-toml"
       ]
     }
   },

diff --git a/book.toml b/book.toml
@@ -32,6 +32,10 @@ edit-url-template = "https://raw.githubusercontent.com/lean-ja/lean-by-example/m
 # 404 ページが正常にはたらくようにするために必要
 site-url = "https://lean-ja.github.io/lean-by-example/"
 
+[output.html.search]
+# 検索したときに、クエリと見出し語が一致していれば見出し語のページがトップに出てくるようにする
+boost-title = 25
+
 [output.html.fold]
 enable = true
 level = 2