Fix problems compiling documentation

[pintos-anon] / doc / texi2html

diff --git a/doc/texi2html b/doc/texi2html
index 30416a6d212d393ccb2848aafae08f7a870ef07d..7cb22fa94bdc576fb31276f26a3eab240e057a7d 100755 (executable)
--- 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)