Re: @includeverbatim causes spurious empty lines in Info and HTML

[Akim Demaille]

Me>    It really ought to be equivalent to inlining the foo file, i.e.,

Karl> I'm not sure @include should be exactly equivalent to inlining.

!

If if does not, it certainly kills part of the usefulness of include :(
And especially that of includeverbatim.

Karl> In your case it should.  But I seem to recall bug reports about
Karl> this, wanting it to at least start a new paragraph 

This is weird: what's wrong with putting an empty line before the
include if that's your intent?  Created new files certainly prevents
some uses of include, while include = inline keeps all the
possibilities.

Karl> Anyway, I'll take a look.

Thanks Karl!  Of course, there is no urgency :)