From: John Ousterhout 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)