aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorcoq2000-07-26 08:54:50 +0000
committercoq2000-07-26 08:54:50 +0000
commitebfb29814ef24c6c5b1fdbd0fb258bdb19005847 (patch)
treeef735ad2432034cea86f17745aefc762ebf17be7 /doc
parentc330f60f1617afcb42cebe2fd2ccf9f330ea4f89 (diff)
dvips -o ==> dvips -o $@
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@572 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
-rw-r--r--doc/Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/Makefile b/doc/Makefile
index 487da84e4b..f4b0c7ef6c 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -28,5 +28,5 @@ clean::
latex $< && latex $<
.dvi.ps:
- dvips $< -o
+ dvips $< -o $@