From 951b33251addefa79d62c4344f2690014dfd62dd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 6 Nov 2015 14:19:06 +0100
Subject: More on how to compile doc.

---
 INSTALL.doc | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/INSTALL.doc b/INSTALL.doc
index 7658800584..2472d2b2a6 100644
--- a/INSTALL.doc
+++ b/INSTALL.doc
@@ -22,8 +22,8 @@ To produce all the documents, the following tools are needed:
   - dvips
   - bibtex
   - makeindex
-  - fig2dev
-  - convert
+  - fig2dev (transfig)
+  - convert (ImageMagick)
   - hevea
   - hacha
 
-- 
cgit v1.2.3