diff --git a/.gitignore b/.gitignore index a732407..52652cb 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,6 @@ # Generated site and pinned toolchain public/ -tools/ +/tools/ # Calepin build artifacts .calepin/ diff --git a/site/calepin.toml b/site/calepin.toml index a01f9d7..0d1a17a 100644 --- a/site/calepin.toml +++ b/site/calepin.toml @@ -63,6 +63,10 @@ item = [ { target = "cs/index.typ" }, { glob = "cs/*" } ] +section = [ + { title = "Tools", item = [{ glob = "cs/tools/*.typ" }] } +] + [[sidebar.section]]