diff --git a/doc/dev_infrastructure/Makefile b/doc/dev_infrastructure/Makefile index 05555d401b0b3ddeadfd24c2ec74047a0520de7e..8c42622e1acc604d6a55595d1bde899aa1f7adb2 100644 --- a/doc/dev_infrastructure/Makefile +++ b/doc/dev_infrastructure/Makefile @@ -1,7 +1,7 @@ # Tools LATEXFLAGS ?= -interaction=nonstopmode -file-line-error PDFLATEX = pdflatex $(LATEXFLAGS) -BIBTEX = bibtex +BIBTEX = FIG2DEV = fig2dev RUBBER ?= $(shell which rubber 2> /dev/null) RUBBERFLAGS = --pdf --short --warn refs --warn misc