# HG changeset patch
# User wenzelm
# Date 939238372 -7200
# Node ID c98d705380330e902576897fb442f20ff0414b60
# Parent  7fab9592384fc9bc4e1087870e88077361c35ec3
ISABELLE_USEDIR_OPTIONS: -d pdf option (off by default);

diff -r 7fab9592384f -r c98d70538033 etc/settings
--- a/etc/settings	Wed Oct 06 18:50:51 1999 +0200
+++ b/etc/settings	Wed Oct 06 21:32:52 1999 +0200
@@ -48,6 +48,7 @@
 ###
 
 ISABELLE_USEDIR_OPTIONS="-i false"
+#ISABELLE_USEDIR_OPTIONS="-i true -d pdf"
 
 
 ###