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

[Zoltan Somogyi]

2023-04-20 18:55 GMT+10:00 "Julien Fischer" <jfischer at opturion.com>:
>>     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.

Done.

>>  <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.

My point is: what is the point of styling it differently? I see no point,
and I think it looks strange.

>> +<!---------
>> +% 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".

I don't think that's a good idea.  Decisions about which notes should be
published should decide just that; they should not require moving files around.

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

Done.

Zoltan.