diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2011-05-05 17:45:55 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2011-05-05 17:45:55 +0000 |
commit | 0f04a21274086f1438aa1598c11437c405ad248f (patch) | |
tree | 5d99fb1e14edd2c98d9e795e5ceb8845085f6f82 /doc/Makefile | |
parent | 6b921c3ac63599ba26aec8a478f23e423b64dc10 (diff) |
Remove mention of dvi
Diffstat (limited to 'doc/Makefile')
-rw-r--r-- | doc/Makefile | 4 |
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). ## ########################################################################### |