From: John Ousterhout <ouster@cs.stanford.edu>
Date: Wed, 28 Mar 2018 16:59:11 +0000 (-0700)
Subject: Fix problems compiling documentation
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=1bdc52e105849c029c8d6e9dfde505a66d91c5da;p=pintos-anon

Fix problems compiling documentation
* Two warnings (deprecated regex syntax)
* One error (couldn't find pintos-t2h.init without "./" prefix)
---

diff --git a/doc/Makefile b/doc/Makefile
index 95dd71b..9e0e994 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -6,7 +6,7 @@ bibliography.texi localsettings.texi
 all: pintos.html pintos.info pintos.pdf
 
 pintos.html: $(TEXIS) texi2html
-	./texi2html -toc_file=$@ -split=chapter -nosec_nav -nomenu -init_file pintos-t2h.init $<
+	./texi2html -toc_file=$@ -split=chapter -nosec_nav -nomenu -init_file ./pintos-t2h.init $<
 
 pintos.info: $(TEXIS)
 	makeinfo $<
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)