book.toml

[book]
authors = ["Seasawher"]
language = "ja"
multilingual = false
src = "booksrc"
title = "Lean Problems"
description = "Lean の問題集"

[build]
create-missing = false
build-dir = "book"

[output.html]
no-section-label = false
git-repository-url = "https://github.com/lean-ja/lean-problems"
edit-url-template = "https://raw.githubusercontent.com/lean-ja/lean-problems/main/{path}"
site-url = "https://lean-ja.github.io/lean-problems/"
additional-js = [
  # Add "Run on Lean4 Playground" button to each code block
  "assets/blockPlay.js",

  # Add "Run on Lean4 Playground" button to each page
  "assets/filePlay.js",

  # Improve search functionality
  "assets/fzf.umd.js",
  "assets/elasticlunr.js",

  # add table of contents to each page
  "assets/pagetoc.js",
]
additional-css = [
  "assets/pagetoc.css",
  "./assets/mdbook-admonish.css"
]

[preprocessor]

[preprocessor.admonish]
command = "mdbook-admonish"
assets_version = "3.0.2" # do not edit: managed by `mdbook-admonish install`