aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/Makefile.doc
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-23 18:05:09 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2010-08-23 18:05:09 +0000
commitbd99ed45eb393b4754d16306ada6d69f05d4fdfd (patch)
treea910755eb2a34e3fc34551bb304c31707c86b67d /doc/Makefile.doc
parent9d8c81aa7f5963964af2a4770975806a8ad45188 (diff)
-prefix -> --output
Diffstat (limited to 'doc/Makefile.doc')
-rw-r--r--doc/Makefile.doc2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/Makefile.doc b/doc/Makefile.doc
index 12e949ea..0e8d1852 100644
--- a/doc/Makefile.doc
+++ b/doc/Makefile.doc
@@ -72,7 +72,7 @@ rearrange:
$(DVI2PS) $< -o $*.ps
.texi.html:
- $(TEXI2HTML) -prefix $* $<
+ $(TEXI2HTML) --output $* $<
default: doc