[m-rev.] for review: improve developer doc web page

[Julien Fischer]

On Thu, 20 Apr 2023, Zoltan Somogyi wrote:

> Fix the developer documentation page.
> 
> development/include/developer.inc:
>     Put the links in the list into order based on "when does a new
>     developer need this?".
>
>     Include a link to the document on the overall design of the Mercury system.
>
>     Comment out links to out-of-date and/or irrelevant-to-developers documents.

I would be inclined to simply delete them rather than comment them out.

>
>     Standardize the format of list entries.
>
>     Add XXXs for other possible changes.
>

...

> diff --git a/development/include/developer.inc b/development/include/developer.inc
> index 830eeec..c1dec27 100644
> --- a/development/include/developer.inc
> +++ b/development/include/developer.inc
> @@ -1,5 +1,10 @@
>  <h2>Development<span class="submenutitle">/ developer documentation</span></h2>
> 
> +<!---------
> +% XXX What is the point of this "submenutitle"?
> +% I this header should just be "Developer documentation".

The title here is "Developement / developer documentation", where the latter bit
(inside the span) is styled differently.

...

> +<!---------
> +% XXX
> +% I (zs) think that we should divide the .html files in the notes directory
> +% into two categories: those that describe how the system currently works, and
> +% everything else. We should include individual links to the files
> +% in the first category above; and we should not include any links
> +% to the files in the second category at all, even via this index.
> +-------->

Or maybe just split the notes directory in two, e.g. "design" and "notes".

You may go ahead and commit this; I will give it a final look over before
I update the web site.

Julien.