equal
deleted
inserted
replaced
1 #!/bin/bash |
|
2 # |
|
3 # $Id$ |
|
4 # |
|
5 # makemainpage -- make main Isabelle web pages |
|
6 |
|
7 TARGET=/usr/proj/isabelle-repository/www |
|
8 FILES="index.html docs.html logics.html cambridge.gif munich.gif" |
|
9 PREFIX=main |
|
10 |
|
11 PRG=$(basename $0) |
|
12 THIS=$(cd $(dirname "$0"); echo $PWD) |
|
13 |
|
14 function usage() |
|
15 { |
|
16 echo |
|
17 echo "Usage: $PRG VERSION DIST" |
|
18 echo |
|
19 cat <<EOF |
|
20 Make Isabelle main web pages with links to documentation for VERSION |
|
21 |
|
22 VERSION should be the Isabelle version contained in DIST |
|
23 DIST should be an Isabelle distribution archive or directory |
|
24 |
|
25 EOF |
|
26 exit 1 |
|
27 } |
|
28 |
|
29 function fail() |
|
30 { |
|
31 echo "$1" >&2 |
|
32 exit 2 |
|
33 } |
|
34 |
|
35 |
|
36 ## process command line |
|
37 |
|
38 [ $# -ne 2 ] && usage |
|
39 |
|
40 export DISTNAME=$1 |
|
41 shift |
|
42 DIST=$1 |
|
43 |
|
44 cd $THIS/page |
|
45 |
|
46 if [ -d $DIST ]; then |
|
47 cp $DIST/doc/Contents . |
|
48 else |
|
49 if [ -f $DIST ]; then |
|
50 gzip -dc $DIST | tar -Bxf - $DISTNAME/doc/Contents |
|
51 mv $DISTNAME/doc/Contents . |
|
52 rmdir -p $DISTNAME/doc |
|
53 else |
|
54 echo error: $DIST not found |
|
55 fail |
|
56 fi |
|
57 fi |
|
58 |
|
59 make main |
|
60 |
|
61 for FILE in $FILES; do |
|
62 cp -f $PREFIX/$FILE $TARGET |
|
63 done |
|
64 |
|
65 chmod g=u $TARGET/* |
|
66 |
|
67 ( cd $TARGET; echo -e "\nYou should find the Isabelle pages in $PWD"; ) |
|