GitLab

Remove the optional arguments from all @node commands: makeinfo can
generate these automatically, and it is easier to edit and rearrange
nodes without them.