On Sun, Nov 13, 2022 at 11:53:54AM +0000, Gavin Smith wrote: > On Sun, Nov 13, 2022 at 12:26:33PM +0100, Patrice Dumas wrote: > > On Sun, Nov 13, 2022 at 11:12:17AM +0000, Gavin Smith wrote: > > > I've done it myself. I didn't change the makeinfo invocation. I don't > > > like the "-c TEXINFO_OUTPUT_FORMAT=plaintexinfo" option much but it is > > > not a big deal if you would rather use it. (My feeling is that > > > "plaintexinfo" is not very descriptive and that the TEXINFO_ prefix > > > is redundant.) > > > > plaintexinfo could be changed to something else, just tell me. > > If we change it to something else then texi2dvi can't use it because > old versions won't have whatever we leave it to.
Can't use it now, but could in the future. If you want another name, we could deprecate plaintexinfo, add the new name, and remove plaintexinfo in 10 years. -- Pat
