author | wenzelm |
Fri, 15 Oct 1999 16:43:05 +0200 | |
changeset 7873 | 5d1200c7a671 |
parent 7872 | 2e2d7e80fb07 |
child 7874 | 180364256231 |
etc/settings | file | annotate | diff | comparison | revisions |
--- 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"