equal
deleted
inserted
replaced
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # |
4 # |
5 # makemainpage -- make main Isabelle web pages |
5 # makemainpage -- make main Isabelle web pages |
6 |
6 |
7 TARGET=/usr/proj/isabelle-repository/web |
7 TARGET=/usr/proj/isabelle-repository/www |
8 FILES="index.html docs.html about.html cambridge.gif munich.gif" |
8 FILES="index.html docs.html about.html cambridge.gif munich.gif" |
9 PREFIX=main |
9 PREFIX=main |
10 |
10 |
11 PRG=$(basename $0) |
11 PRG=$(basename $0) |
12 THIS=$(cd $(dirname "$0"); echo $PWD) |
12 THIS=$(cd $(dirname "$0"); echo $PWD) |