From: Ben Pfaff Date: Tue, 21 Jun 2005 03:59:08 +0000 (+0000) Subject: texi2html doesn't support @verbatiminclude, so kluge it. X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pintos-anon;a=commitdiff_plain;h=629ddac81289018a0ab9caa723ae876f3b44eb64 texi2html doesn't support @verbatiminclude, so kluge it. --- diff --git a/doc/.cvsignore b/doc/.cvsignore index cb7722e..ba565ea 100644 --- a/doc/.cvsignore +++ b/doc/.cvsignore @@ -18,3 +18,4 @@ pintos.html pintos.pdf pintos.ps pintos_*.html +sample.tmpl.texi diff --git a/doc/Makefile b/doc/Makefile index 371e366..e06d528 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -1,6 +1,6 @@ TEXIS = pintos.texi intro.texi tour.texi threads.texi userprog.texi \ vm.texi filesys.texi references.texi standards.texi doc.texi \ -sample.tmpl devel.texi debug.texi 44bsd.texi +sample.tmpl.texi devel.texi debug.texi 44bsd.texi all: pintos.html pintos.info pintos.dvi pintos.ps pintos.pdf @@ -19,6 +19,9 @@ pintos.ps: pintos.dvi pintos.pdf: $(TEXIS) texi2pdf $< -o $@ +%.texi: % + sed < $< > $@ 's/\([{}@]\)/\@\1/g;' + clean: rm -f *.info *.html rm -f *.dvi *.pdf *.ps *.log *~ diff --git a/doc/doc.texi b/doc/doc.texi index 90edb1e..c43a5bb 100644 --- a/doc/doc.texi +++ b/doc/doc.texi @@ -54,4 +54,6 @@ joins @var{B}, then @var{A} joins @var{C}), and so on. @node Sample Design Document @section Sample Design Document -@verbatiminclude sample.tmpl +@example +@include sample.tmpl.texi +@end example