# HG changeset patch
# User wenzelm
# Date 1238965959 -7200
# Node ID 0a667739d175f9bbb8c24d36c3a31b7330660126
# Parent  71fde5b7b43c421bd38cd081152865750f693653# Parent  104b13484feb9a8abe5a9f500432019bbac04d30
merged

diff -r 71fde5b7b43c -r 0a667739d175 Admin/makedist
--- a/Admin/makedist	Sun Apr 05 19:21:51 2009 +0100
+++ b/Admin/makedist	Sun Apr 05 23:12:39 2009 +0200
@@ -125,17 +125,6 @@
 cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
 
 
-# website
-
-mkdir -p ../website
-cat > ../website/config <<EOF
-DISTNAME="$DISTNAME"
-DISTBASE="$DISTBASE"
-EOF
-
-cp lib/html/library_index_content.template ../website/
-
-
 # prepare dist for release
 
 echo "###"
diff -r 71fde5b7b43c -r 0a667739d175 doc-src/pdfsetup.sty
--- a/doc-src/pdfsetup.sty	Sun Apr 05 19:21:51 2009 +0100
+++ b/doc-src/pdfsetup.sty	Sun Apr 05 23:12:39 2009 +0200
@@ -1,9 +1,8 @@
-%% $Id$
 %%
 %% hyperref setup -- special version for Isabelle documentation
 %%
 
-\message{pdfsetup.sty v0.4 2008-05-15}
+\usepackage{ifpdf}
 
 \usepackage{color}
 \definecolor{linkcolor}{rgb}{0,0,0}
@@ -14,3 +13,5 @@
 \gdef\bold#1{\textbf{\hyperpage{#1}}}
 
 \urlstyle{rm}
+
+\ifpdf\relax\else\renewcommand{\url}[1]{\nolinkurl{#1}}\fi
\ No newline at end of file