| changeset 7873 | 5d1200c7a671 |
| parent 7864 | 5cd5a27f5c93 |
| child 8345 | e708af969264 |
--- a/etc/settings Fri Oct 15 15:31:35 1999 +0200 +++ b/etc/settings Fri Oct 15 16:43:05 1999 +0200 @@ -61,7 +61,7 @@ ISABELLE_BIBTEX="bibtex" ISABELLE_DVIPS="dvips -D 600" -# The thumpdf tool is probably not generally available ... +# The thumbpdf tool is probably not generally available ... #ISABELLE_THUMBPDF="thumbpdf"