equal
deleted
inserted
replaced
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 |