Looks like a bug...

Yes it does.  I wonder if you put a blank line after @Deffn ...

    PS: I would like to have `@end Deffn' instead of `@end deffn'.  How
        can I do that?

I don't see how this would be possible.  Sorry.

Reply via email to