\header {
texidoc = "Notes that are shorter than the common shortest note get a
space (i.e. without the space needed for the note) proportional to
\header {
texidoc = "Notes that are shorter than the common shortest note get a
space (i.e. without the space needed for the note) proportional to