Revision 1885931

Merge r1877794 from trunk:

 * r1877794
   Use Doxygen comment leader for comments with doxygen syntax.
   Justification:
     Improve $EDITOR's syntax highlighting.
   Votes:
     +0: danielsh
     +1: brane, jamessan