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

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)