doc: Disable mdbook-pagetoc plugin

mdBook is updated to 0.4.41 along with the nixpkgs' version bump, which has broken mdbook-pagetoc plugin. Let's disable the plugin for now to get the documentation up and running as soon as possible. Signed-off-by: Ivan Nikolaenko <[email protected]>
tiiuae · Jan 27, 2025 · 9e47e15 · 9e47e15
1 parent 40a9c24
commit 9e47e15
Show file tree

Hide file tree

Showing 5 changed files with 0 additions and 720 deletions.
diff --git a/LICENSES/WTFPL.txt b/LICENSES/WTFPL.txt
diff --git a/docs/book.toml b/docs/book.toml
@@ -14,8 +14,6 @@ src = "src"
 default-theme = "light"
 git-repository-url = "https://github.com/tiiuae/ghaf"
 git-repository-icon = "fa-github"
-additional-css = ["theme/pagetoc.css"]
-additional-js = ["theme/pagetoc.js"]
 
 [preprocessor.alerts]