Re: @setfilename: for info only?

[Karl Berry]

    I am not sure that we should decide ourselves for a specific name, I
    think that in most cases the usere will only use one possibility of
    splitting,

I suppose so, although it seems wrong in principle to me to use the same
output name.  html_node, html_chapter?  Oh, yuck, we probably don't want
to change this.

    If .dbk is recognized as docbook, then it would make sense to use it,
    but in my experience docbook docs are always ending in .xml.

Googling around shows some .dbk usage.  I gather people's experiences
differ.  I renamed most/all of the docbook license files on gnu.org to
use .dbk after some discussion with Noah.  .xml is basically meaningless
(we shouldn't use it for Texinfo XML either), while .dbk is clear.

    It is not that problematic to have the xml output and the docbook 
    output ending with the same extension, 

As with the different html splits, I think it's completely wrong in
principle, but probably not worth the hassle for users to change now,
since I unfortunately didn't notice at the time I first integrated the
support for it.

Thanks,
karl