mirror
/
rustc-dev-guide
mirror of https://github.com/rust-lang/rustc-dev-guide.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

enable AND search (#1607)

This commit is contained in:
Tshepang Mbambo 2023-02-18 15:20:26 +02:00 committed by GitHub
parent c1de1a3127
commit e4aafcdccd
1 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
book.toml
View File

@ -18,6 +18,9 @@ git-repository-url = "https://github.com/rust-lang/rustc-dev-guide"
edit-url-template = "https://github.com/rust-lang/rustc-dev-guide/edit/master/{path}" edit-url-template = "https://github.com/rust-lang/rustc-dev-guide/edit/master/{path}"
additional-js = ["mermaid.min.js", "mermaid-init.js"] additional-js = ["mermaid.min.js", "mermaid-init.js"]
[output.html.search]
use-boolean-and = true
[output.html.fold] [output.html.fold]
enable = true enable = true
level = 0 level = 0