X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pintos-anon;a=blobdiff_plain;f=doc%2Ftexi2html;h=7cb22fa94bdc576fb31276f26a3eab240e057a7d;hp=30416a6d212d393ccb2848aafae08f7a870ef07d;hb=c3f2bdb4fcd99dca631962dccb21214e2847f3a3;hpb=1bc4f6f7b325a177e7ddf0d7039cb5c7921dd721

diff --git a/doc/texi2html b/doc/texi2html
index 30416a6..7cb22fa 100755
--- a/doc/texi2html
+++ b/doc/texi2html
@@ -6163,7 +6163,7 @@ sub substitute_style
     {
         $changed = 0;
         $done = '';
-        while (/\@(\w+){([^\{\}]+)}/ || /\@(,){([^\{\}]+)}/)
+        while (/\@(\w+)\{([^\{\}]+)}/ || /\@(,)\{([^\{\}]+)}/)
         {
             $text = &apply_style($1, $2);
             if ($text)