--- 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