Admin/make_everything
changeset 16301 f9f2e1643593
parent 12721 226fc0e2e7e3
child 16328 49c1f9dedc56
equal deleted inserted replaced
16300:a4e163c7ed9c 16301:f9f2e1643593
    31 esac
    31 esac
    32 
    32 
    33 cd $(dirname "$ISABELLE_DIST")
    33 cd $(dirname "$ISABELLE_DIST")
    34 cp -a ../contrib .
    34 cp -a ../contrib .
    35 
    35 
    36 cd page && make
    36 cd website && make && cd .. && rm -rf website
    37 cd .. && rm -rf page
       
    38 
    37 
    39 date
    38 date