Admin/make_everything
changeset 16301 f9f2e1643593
parent 12721 226fc0e2e7e3
child 16328 49c1f9dedc56
     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