From aa1bc955fb5428e15da5906027d8a24b2d344a0c Mon Sep 17 00:00:00 2001 From: Paul-Elliot Date: Tue, 19 Nov 2024 18:15:08 +0100 Subject: [PATCH] Sidebar: Use a better name when no zero title are there --- src/document/sidebar.ml | 11 ++++++++++- src/driver/odoc_driver.ml | 2 +- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/src/document/sidebar.ml b/src/document/sidebar.ml index 452ba4dfb4..c84904d565 100644 --- a/src/document/sidebar.ml +++ b/src/document/sidebar.ml @@ -86,7 +86,16 @@ end = struct match Comment.find_zero_heading entry.doc with | Some t -> t | None -> - Location_.[ at (span []) (`Word (Id.name entry.id)) ] + let name = + match entry.id.iv with + | `LeafPage (Some parent, name) + when String.equal + (Names.PageName.to_string name) + "index" -> + Id.name parent + | _ -> Id.name entry.id + in + Location_.[ at (span []) (`Word name) ] in Comment.link_content title | _ -> diff --git a/src/driver/odoc_driver.ml b/src/driver/odoc_driver.ml index 43f841872f..4d5e72a730 100644 --- a/src/driver/odoc_driver.ml +++ b/src/driver/odoc_driver.ml @@ -258,7 +258,7 @@ let run mode (* Grep log index and co commands *) grep_log `Count_occurrences index_grep; grep_log `Count_occurrences index_grep; - grep_log `Index (* index_grep *) (Some ""); + grep_log `Index index_grep; List.iter (fun { Cmd_outputs.log_dest; prefix; run } ->