--- a/etc/settings Thu Oct 14 15:01:18 1999 +0200 +++ b/etc/settings Thu Oct 14 15:02:04 1999 +0200 @@ -61,6 +61,9 @@ ISABELLE_BIBTEX="bibtex" ISABELLE_DVIPS="dvips -D 600" +# The thumpdf tool is probably not generally available ... +#ISABELLE_THUMBPDF="thumbpdf" + ### ### Misc path settings