# HG changeset patch
# User wenzelm
# Date 939906124 -7200
# Node ID 5cd5a27f5c9380e62f013c711d96dc77672c9c25
# Parent  8b0aca9bdc26dfbaa1367a23eac3ce8186c573c4
thumbpdf (disabled by default);

diff -r 8b0aca9bdc26 -r 5cd5a27f5c93 etc/settings
--- 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