More on how to compile doc.

herbelin · herbelin · commit 951b33251add · 2015-11-06T14:27:11.000+01:00
diff --git 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
 
