diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-06 14:19:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-06 14:27:11 +0100 |
| commit | 951b33251addefa79d62c4344f2690014dfd62dd (patch) | |
| tree | 090df92fc2fec09c0f982d4bca5fe85168823e3d /INSTALL.doc | |
| parent | 6b3d6f9326de9e53805d14e78577411c7174a998 (diff) | |
More on how to compile doc.
Diffstat (limited to 'INSTALL.doc')
| -rw-r--r-- | INSTALL.doc | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/INSTALL.doc b/INSTALL.doc index 765880058..2472d2b2a 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 |