X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;ds=inline;f=doc%2FMakefile;h=95dd71bdf0e6c5a0dfed6a06f0c6bdd60228df2a;hb=1e8cf142b66f74cd5214c64294d0320fb2d9f4fa;hp=44b20992c2b3f47d60744884084c05936e7e66f9;hpb=8d6b5c9e4c160c7e74de26c80a31f18bd5df5884;p=pintos-anon diff --git a/doc/Makefile b/doc/Makefile index 44b2099..95dd71b 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -1,9 +1,9 @@ TEXIS = pintos.texi intro.texi threads.texi userprog.texi vm.texi \ filesys.texi license.texi reference.texi 44bsd.texi standards.texi \ doc.texi sample.tmpl.texi devel.texi debug.texi installation.texi \ -bibliography.texi +bibliography.texi localsettings.texi -all: pintos.html pintos.info pintos.dvi pintos.ps pintos.pdf +all: pintos.html pintos.info pintos.pdf pintos.html: $(TEXIS) texi2html ./texi2html -toc_file=$@ -split=chapter -nosec_nav -nomenu -init_file pintos-t2h.init $< @@ -27,9 +27,10 @@ pintos.pdf: $(TEXIS) sed < $< > $@ 's/\([{}@]\)/\@\1/g;' clean: - rm -f *.info *.html + rm -f *.info* *.html rm -f *.dvi *.pdf *.ps *.log *~ rm -rf WWW + rm -f sample.tmpl.texi dist: pintos.html pintos.pdf rm -rf WWW