Add plaintext target.

diff --git a/doc/Makefile b/doc/Makefile
index e06d52832b5598e5ae364d048b574513c2eba640..eb5c68e8421933175214e93d2561da6035aefa10 100644 (file)
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -10,6 +10,9 @@ pintos.html: $(TEXIS) texi2html
 pintos.info: $(TEXIS)
        makeinfo $<
 
+pintos.text: $(TEXIS)
+       makeinfo --plaintext -o $@ $<
+
 pintos.dvi: $(TEXIS)
        texi2dvi $< -o $@