From 45779d74209a728cfd67628eaa53b42fee129f65 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Mon, 17 Aug 2015 15:58:18 +0200
Subject: Remove generatable documentation files from repository. (Fix bug
 #4315)

---
 Makefile.common | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index de26eeb9b..8f3d39bf2 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -109,7 +109,11 @@ LATEX:=latex
 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:=simple
-- 
cgit v1.2.3