DescriptionUse @dots{} instead of ... in notation manual where appropriate
This uses a typographically preferable variant, and also may render
better in Info format in some circumstances.
Patch Set 1 #
Total comments: 17
Patch Set 2 : Also treat instances of .. #
MessagesTotal messages: 7
|