You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We should only give (unnumbered) titles, subtitles, etc and, if need be, the numbering and the table of content should be automatically written by some tool.
I can write some crude sh/awk/sed helpers, but maybe the format should stabilize before.