Admin/make_everything
author wenzelm
Wed Sep 21 20:16:34 2005 +0200 (2005-09-21)
changeset 17572 81fcc0029761
parent 16328 49c1f9dedc56
permissions -rwxr-xr-x
tuned;
wenzelm@12721
     1
#!/usr/bin/env bash
wenzelm@11121
     2
#
wenzelm@11121
     3
# $Id$
wenzelm@11121
     4
#
wenzelm@11121
     5
# make_everything -- an adhoc script that demonstrates the general procedure
haftmann@16328
     6
#   of creating the Isabelle distribution and WWW site
wenzelm@11121
     7
#
wenzelm@11121
     8
# assumptions:
wenzelm@11121
     9
#   - proper settings for polyml are present by magic
wenzelm@11121
    10
#     (e.g. via ~/isabelle/etc/settings)
wenzelm@11121
    11
#   - ~/tmp/isadist/contrib holds packages of external tools (polyml etc.)
haftmann@16328
    12
wenzelm@11121
    13
wenzelm@11121
    14
date
wenzelm@11121
    15
wenzelm@11121
    16
REPOS=~/isabelle/src
wenzelm@11121
    17
DIST=~/tmp/isadist
wenzelm@11121
    18
wenzelm@17572
    19
$REPOS/Admin/makedist ${1:--}
wenzelm@11121
    20
ISABELLE_DIST=$(cat $DIST/ISABELLE_DIST)
wenzelm@11121
    21
wenzelm@11121
    22
case $(hostname) in
wenzelm@11121
    23
  *broy*)
wenzelm@11121
    24
    #Note: this causes strange behaviour with "nohup" -- better use "screen"
wenzelm@11121
    25
    ssh sunbroy1 ". ~/.bashrc; $REPOS/Admin/makebin $ISABELLE_DIST"
wenzelm@11121
    26
    ssh atbroy37 ". ~/.bashrc; $REPOS/Admin/makebin $ISABELLE_DIST"
wenzelm@11121
    27
    ;;
wenzelm@11121
    28
  *)
wenzelm@11121
    29
    $REPOS/Admin/makebin $ISABELLE_DIST
wenzelm@11121
    30
    ;;
wenzelm@11121
    31
esac
wenzelm@11121
    32
wenzelm@11121
    33
cd $(dirname "$ISABELLE_DIST")
wenzelm@11121
    34
cp -a ../contrib .
wenzelm@11121
    35
haftmann@16301
    36
cd website && make && cd .. && rm -rf website
wenzelm@11121
    37
wenzelm@11121
    38
date