Re: @deffn without index

[Karl Berry]

    Not a real `problem'.  But it litters the environment with unused
    files (i.e. if there is no @printindex command), and I don't like this
    very much.  Maybe this is me only.

Oh, I agree the extra empty files are annoying, but it is hard to fix.

There was a patch for this sent years ago but it was intertwined with
other issues.  At some point I'll see if I can dig it out and extract
out the relevant pieces.