diff options
| author |  emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-06 16:27:13 +0000 |
|---|---|---|
| committer | emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-06 16:27:13 +0000 |
| commit | 015e33fb137c89ba96b2806f828cd47341c3bd92 (patch) | |
| tree | 0e440637fb430a0aaf343de48df26c07bd570435 /Makefile.doc | |
| parent | 7eda1af42c6634d5d27a019d2da9f1ae98c0e170 (diff) | |
Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for pngtopnm and pnmtops
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13401 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/Makefile.doc b/Makefile.doc index 56daaa851..584e25394 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -56,9 +56,6 @@ endif %.ps: %.dvi (cd `dirname $<`; dvips -q -o `basename $@` `basename $<`) -%.eps: %.png - pngtopnm $< | pnmtops -equalpixels -noturn -rle > $@ - ###################################################################### # Macros for filtering outputs ###################################################################### |