aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/Makefile
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2011-05-05 17:45:55 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2011-05-05 17:45:55 +0000
commit0f04a21274086f1438aa1598c11437c405ad248f (patch)
tree5d99fb1e14edd2c98d9e795e5ceb8845085f6f82 /doc/Makefile
parent6b921c3ac63599ba26aec8a478f23e423b64dc10 (diff)
Remove mention of dvi
Diffstat (limited to 'doc/Makefile')
-rw-r--r--doc/Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/Makefile b/doc/Makefile
index 0331cd10..85d44fb4 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -10,8 +10,8 @@
###########################################################################
##
## Use:
-## make info,dvi,pdf,html - build respective docs from texi source.
-## make doc - make default kinds of doc (dvi, info).
+## make info,pdf,html - build respective docs from texi source.
+## make doc - make default kinds of doc (, info).
##
###########################################################################