diff options
| author | Emilio Jesus Gallego Arias | 2018-04-28 23:47:34 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-04-28 23:47:34 +0200 |
| commit | 9f05901696feba9c970c3385af08b4779aae9078 (patch) | |
| tree | 55c0c3aec2459ef3f43321d791b2947f849bd243 /Makefile.doc | |
| parent | a76730b8479b9036e814cc3ff5e7f32d46fc942c (diff) | |
[doc] Remove unused dependencies.
AFAICS `imagemagick` `hacha` and `transfig` are not used anymore.
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/Makefile.doc b/Makefile.doc index ce31c5fcbe..9b6013d8d7 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -32,10 +32,7 @@ BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10 MAKEINDEX:=makeindex PDFLATEX:=pdflatex DVIPS:=dvips -FIG2DEV:=fig2dev -CONVERT:=convert HEVEA:=hevea -HACHA:=hacha HEVEAOPTS:=-fix -exec xxdate.exe HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea HTMLSTYLE:=coqremote @@ -110,20 +107,6 @@ endif %.ps: %.dvi (cd `dirname $<`; $(DVIPS) -q -o `basename $@` `basename $<`) -%.png: %.fig - $(FIG2DEV) -L png -m 2 $< $@ - -%.pdf: %.fig - $(FIG2DEV) -L pdftex $< $@ - $(FIG2DEV) -L pdftex_t -p `basename $@` $< $@_t - -%.eps: %.fig - $(FIG2DEV) -L pstex $< $@ - $(FIG2DEV) -L pstex_t -p `basename $@` $< $@_t - -%.eps: %.png - $(CONVERT) $< $@ - ###################################################################### # Macros for filtering outputs ###################################################################### |