merged
authorwenzelm
Sun, 05 Apr 2009 23:12:39 +0200
changeset 308720a667739d175
parent 30869 71fde5b7b43c
parent 30871 104b13484feb
child 30873 105e887994d0
merged
     1.1 --- a/Admin/makedist	Sun Apr 05 19:21:51 2009 +0100
     1.2 +++ b/Admin/makedist	Sun Apr 05 23:12:39 2009 +0200
     1.3 @@ -125,17 +125,6 @@
     1.4  cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
     1.5  
     1.6  
     1.7 -# website
     1.8 -
     1.9 -mkdir -p ../website
    1.10 -cat > ../website/config <<EOF
    1.11 -DISTNAME="$DISTNAME"
    1.12 -DISTBASE="$DISTBASE"
    1.13 -EOF
    1.14 -
    1.15 -cp lib/html/library_index_content.template ../website/
    1.16 -
    1.17 -
    1.18  # prepare dist for release
    1.19  
    1.20  echo "###"
     2.1 --- a/doc-src/pdfsetup.sty	Sun Apr 05 19:21:51 2009 +0100
     2.2 +++ b/doc-src/pdfsetup.sty	Sun Apr 05 23:12:39 2009 +0200
     2.3 @@ -1,9 +1,8 @@
     2.4 -%% $Id$
     2.5  %%
     2.6  %% hyperref setup -- special version for Isabelle documentation
     2.7  %%
     2.8  
     2.9 -\message{pdfsetup.sty v0.4 2008-05-15}
    2.10 +\usepackage{ifpdf}
    2.11  
    2.12  \usepackage{color}
    2.13  \definecolor{linkcolor}{rgb}{0,0,0}
    2.14 @@ -14,3 +13,5 @@
    2.15  \gdef\bold#1{\textbf{\hyperpage{#1}}}
    2.16  
    2.17  \urlstyle{rm}
    2.18 +
    2.19 +\ifpdf\relax\else\renewcommand{\url}[1]{\nolinkurl{#1}}\fi
    2.20 \ No newline at end of file