# HG changeset patch
# User wenzelm
# Date 939998585 -7200
# Node ID 5d1200c7a67158ed0c69ac27ffff0ac5444095b7
# Parent  2e2d7e80fb07c13953c3faf88477651c0418d1c0
fixed comment;

diff -r 2e2d7e80fb07 -r 5d1200c7a671 etc/settings
--- 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"