From b99d61c6b8feae87add7443c510531ed573e986a Mon Sep 17 00:00:00 2001 From: Jules Aguillon Date: Fri, 10 Nov 2023 12:42:29 +0100 Subject: [PATCH] Remove the "index" tentative fix It's not possible to reference the package main page and this cannot be fixed now by tweaking the convention. --- doc/parent_child_spec.mld | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/doc/parent_child_spec.mld b/doc/parent_child_spec.mld index 5658b5d3a4..16b5b0e561 100644 --- a/doc/parent_child_spec.mld +++ b/doc/parent_child_spec.mld @@ -180,12 +180,8 @@ following convention should be followed. - A page is the parent of every installed pages. The driver can freely name this page, for example it can be named after the package. In what follows, we refer to this page as the [pkg] page. -- If there is an installed [index.mld] file: - + The driver has to use it as content for the [pkg] page. - + The can decide to also include a [index] page as child of the [pkg] page. - - If it does not, then some references to the [index] page might be - unresolved. - - If it does, it will create a warning. +- If there is an installed [index.mld] file, the driver has to use it as + content for the [pkg] page. - If there is no installed [index.mld] page, the driver has to generate some content for the [pkg] page.