diff options
author | Dimitri van Heesch <dimitri@stack.nl> | 2007-03-15 10:14:23 (GMT) |
---|---|---|
committer | Dimitri van Heesch <dimitri@stack.nl> | 2007-03-15 10:14:23 (GMT) |
commit | cc52853c15833c9a18be11c140b99d94d9e06e9e (patch) | |
tree | 5300b179faf00eea740dda6ee3be5343c70b1c79 /src/commentcnv.l | |
parent | eb591296685b8268427173e0a24f74abd987170d (diff) | |
download | Doxygen-cc52853c15833c9a18be11c140b99d94d9e06e9e.zip Doxygen-cc52853c15833c9a18be11c140b99d94d9e06e9e.tar.gz Doxygen-cc52853c15833c9a18be11c140b99d94d9e06e9e.tar.bz2 |
Release-1.5.1-20070315
Diffstat (limited to 'src/commentcnv.l')
-rw-r--r-- | src/commentcnv.l | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/commentcnv.l b/src/commentcnv.l index 25a0f1a..238e56b 100644 --- a/src/commentcnv.l +++ b/src/commentcnv.l @@ -323,7 +323,7 @@ CHARLIT (("'"\\[0-7]{1,3}"'")|("'"\\."'")|("'"[^' \\\n]{1,4}"'")) copyToOutput(yytext,yyleng); BEGIN(CComment); } -<CComment,ReadLine>[\\@]("dot"|"code")/[^a-z_A-Z0-9] { /* start of a verbatim block */ +<CComment,ReadLine>[\\@]("dot"|"code"|"msc")/[^a-z_A-Z0-9] { /* start of a verbatim block */ copyToOutput(yytext,yyleng); g_lastCommentContext = YY_START; g_blockName=&yytext[1]; @@ -352,7 +352,7 @@ CHARLIT (("'"\\[0-7]{1,3}"'")|("'"\\."'")|("'"[^' \\\n]{1,4}"'")) <Scan>. { /* any other character */ copyToOutput(yytext,yyleng); } -<Verbatim>[\\@]("endverbatim"|"endlatexonly"|"endhtmlonly"|"endxmlonly"|"endrtfonly"|"endmanonly"|"enddot"|"endcode"|"f$"|"f]"|"f}") { /* end of verbatim block */ +<Verbatim>[\\@]("endverbatim"|"endlatexonly"|"endhtmlonly"|"endxmlonly"|"endrtfonly"|"endmanonly"|"f$"|"f]"|"f}") { /* end of verbatim block */ copyToOutput(yytext,yyleng); if (yytext[1]=='f') // end of formula { @@ -363,7 +363,7 @@ CHARLIT (("'"\\[0-7]{1,3}"'")|("'"\\."'")|("'"[^' \\\n]{1,4}"'")) BEGIN(g_lastCommentContext); } } -<VerbatimCode>[\\@]("enddot"|"endcode") { /* end of verbatim block */ +<VerbatimCode>[\\@]("enddot"|"endcode"|"endmsc") { /* end of verbatim block */ copyToOutput(yytext,yyleng); if (&yytext[4]==g_blockName) { |