Re: makeinfo options

[Karl Berry]

    Nowadays, the missing features are mostly there, but I'm not sure it's
    a good idea to break back compatibility.  

We shouldn't change the behavior of --no-headers, that would break
existing Makefiles.  However, we could invent a new option, --plaintext
or some such, that has different behavior.  Actually I think the output
formats should have another option, --output-format=FORMAT, instead of a
separate option for each format.  But anyway ...