Minutes updated + some hints for all (Re: suggested changes to minutes of 2023 March 09)

Thank you Peter, the changes have been applied.

FTR, I took the liberty of applying them despite the fact that the 
minutes had been approved already, since the changes are purely 
editorial (adding subtopics).

For all, and for future references:

* some W3C colleagues explained to me how to easily insert 
topics/subtopic (actually, any line) in the log directly from IRC: 
similar to s/.../.../ for substitution, there is an i/.../.../ command 
for insertion!
   It is in the scribing documentationn but well hidden (Step 3, second 
to last item <https://w3c.github.io/scribe2/scribedoc.html#notes>)

* if you want to patch IRC logs after the fact, as Peter just did:

   - notice that the script generating the minutes ignores timestamps; 
you don't even have to put them in the lines you add
   - however, the script cares about who says what, so in the lines you 
add, you need to add a "speaker", in pointy brackets (best option is to 
put your own nickname)

e.g. those will work

12:34:56 <pchampin> topic: some topic added after the fact
<pchampin> topic: some topic added after the fact

but this one will not

12:34:56 topic: some topic added after the fact

   best

On 16/03/2023 17:57, Peter F. Patel-Schneider wrote:
> I have a couple of suggestions for additions to the minutes of 2023 
> March 09.
>
> I downloaded the text IRC and added two subtopics.  The result is 
> included below.
>
> peter