GitLab

  Make a few cleanups.
  Add extra `help-echo' and `local-map' props to node xrefs.
  Use header-specific faces for node-names & xrefs.
(Info-use-header-line, Info-header-line):
  New variables.
(info-header, info-header-xref, info-header-node):
  New faces.
(Info-setup-header-line):
  New function.
(Info-select-node):
  Call Info-setup-header-line when enabled.
(Info-extract-pointer):
  Work even if the header line is hidden.