From: Ben Pfaff <blp@cs.stanford.edu>
Date: Sun, 26 Sep 2004 21:11:34 +0000 (+0000)
Subject: Fix texi2html options.
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=cc409b1863cc91b6a2dbfc963d221ab548132762;p=pintos-anon

Fix texi2html options.
---

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