From: Ben Pfaff 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