migrated scripts to new webiste
authorhaftmann
Mon Jun 06 14:12:07 2005 +0200 (2005-06-06)
changeset 16301f9f2e1643593
parent 16300 a4e163c7ed9c
child 16302 322e2a3335d4
migrated scripts to new webiste
Admin/make_everything
Admin/makedist
     1.1 --- a/Admin/make_everything	Mon Jun 06 14:11:05 2005 +0200
     1.2 +++ b/Admin/make_everything	Mon Jun 06 14:12:07 2005 +0200
     1.3 @@ -33,7 +33,6 @@
     1.4  cd $(dirname "$ISABELLE_DIST")
     1.5  cp -a ../contrib .
     1.6  
     1.7 -cd page && make
     1.8 -cd .. && rm -rf page
     1.9 +cd website && make && cd .. && rm -rf website
    1.10  
    1.11  date
     2.1 --- a/Admin/makedist	Mon Jun 06 14:11:05 2005 +0200
     2.2 +++ b/Admin/makedist	Mon Jun 06 14:12:07 2005 +0200
     2.3 @@ -161,11 +161,20 @@
     2.4  
     2.5  cd "$DISTBASE/$DISTNAME" || fail "Something is wrong: dist directory doesn't exist!"
     2.6  
     2.7 -cp -R Admin/page ..
     2.8 -cp Distribution/doc/Contents ../page
     2.9 -cp Distribution/lib/logo/isabelle.gif ../page/main-content
    2.10 -cp Distribution/lib/logo/isabelle.gif ../page/dist-content
    2.11 -echo "$DISTNAME" > ../page/DISTNAME
    2.12 +#~ # old site framework
    2.13 +#~ cp -R Admin/page ..
    2.14 +#~ cp Distribution/doc/Contents ../page
    2.15 +#~ cp Distribution/lib/logo/isabelle.gif ../page/main-content
    2.16 +#~ cp Distribution/lib/logo/isabelle.gif ../page/dist-content
    2.17 +#~ echo "$DISTNAME" > ../page/DISTNAME
    2.18 +# new site framework
    2.19 +cp -R Admin/website ..
    2.20 +mkdir -p ../website/conf
    2.21 +cat > ../website/conf/distname.mak <<EOF
    2.22 +# this is a generated file - do not edit unless you know what you are doing
    2.23 +
    2.24 +DISTNAME=$DISTNAME
    2.25 +EOF
    2.26  
    2.27  MOVE=$($FIND Doc \( -type f -a -not -type l -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
    2.28  mv -f $MOVE Distribution/doc