I forgot to check your PR before editing and ended up making a similar change. Sorry about that.

Also, manually editing the .html file will just be overwritten the next time the file is generated, leading to surprising changes for the next CL. It's better to update the <pre class="anchors"> section.

I forgot to check your PR before editing and ended up making a similar change. Sorry about that.

No worries.

Also, manually editing the .html file will just be overwritten the next time the file is generated, leading to surprising changes for the next CL.

I was not sure if the spec auto-builds, but in any event I didn't expect my direct edits of the .html to survive...

I figured it would be useful to put something approximating the output into HTML form for ease of reading, and doing that edit was quicker and easier than building for me in this case.