From cc409b1863cc91b6a2dbfc963d221ab548132762 Mon Sep 17 00:00:00 2001
From: Ben Pfaff <blp@cs.stanford.edu>
Date: Sun, 26 Sep 2004 21:11:34 +0000
Subject: [PATCH 1/1] Fix texi2html options.

---
 doc/Makefile | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/doc/Makefile b/doc/Makefile
index 6b4ce8f..cfb7cbf 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -4,16 +4,16 @@ filesys.texi vm.texi standards.texi doc.texi devel.texi debug.texi
 all: projects.html projects.info
 
 projects.html: $(TEXIS) mlfqs1.png mlfqs2.png
-	./texi2html -toc_file=$@ -split=chapter -no-sec_nav -no-menu -init_file pintos-t2h.init -no-number $<
+	./texi2html -toc_file=$@ -split=chapter -nosec_nav -nomenu -init_file pintos-t2h.init -nonumber $<
 
 projects.info: $(TEXIS)
 	makeinfo $<
 
 %.eps: %.jgr
-	jgraph $< > $@.tmp && mv $@.tmp $@
+	(jgraph $< > $@.tmp && mv $@.tmp $@) || touch $@
 
 %.png: %.eps
 	convert $< $@
 
 clean:
-	rm -f *.info *.html *.eps *.png
+	rm -f *.info *.html *.png
-- 
2.30.2