merged
authorwenzelm
Sun, 05 Apr 2009 23:12:39 +0200
changeset 30872 0a667739d175
parent 30869 71fde5b7b43c (current diff)
parent 30871 104b13484feb (diff)
child 30873 105e887994d0
merged
--- 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 "###"
--- 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