Prior to this change, I think the titles would be links themselves (so you could click on them to have the anchor appear in the navigation bar), whereas after this I think the anchors would be purely hidden? Does that line up with your expectation? I think maybe being able to click can sometimes help people to discover/remember the anchors, but maybe it's more trouble than it is worth as your version certainly makes the raw output more readable. What do you think?
I only wanted a cosmetic change, didn't want to remove the functionality provided by named anchor tags. That's why I revised and overwritten my previous commit.
Prior to this change, I think the titles would be links themselves (so you could click on them to have the anchor appear in the navigation bar), whereas after this I think the anchors would be purely hidden? Does that line up with your expectation? I think maybe being able to click can sometimes help people to discover/remember the anchors, but maybe it's more trouble than it is worth as your version certainly makes the raw output more readable. What do you think?