X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=doc%2FMakefile;h=e06d52832b5598e5ae364d048b574513c2eba640;hb=629ddac81289018a0ab9caa723ae876f3b44eb64;hp=371e366a1cd55408712c356d3b0734b89e554e2a;hpb=92740b65a0ae8c43bfad425fbf2db4bcbd3320ea;p=pintos-anon

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 *~