> > # makeinfo --version > > makeinfo (GNU texinfo) 4.11 > > Someone else filed a PR about this last night. It's fixed on trunk. > Joel, what do you think we should do? Just document it? Can we also put the fix on the branch for later on, when we produce the 6.7.1? -- Joel