Admin/Release/mirror-website
author wenzelm
Fri, 27 Jan 2023 15:22:26 +0100
changeset 77108 4f68b165d69e
parent 74916 79ceca45fcbc
permissions -rwxr-xr-x
back to Scala 3.2.0 for now, since 3.2.1 causes odd crash of REPL concerning value classes (e.g. "isabelle.Time.now()"); enforce rebuild of Isabelle/ML + Isabelle/Scala;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17671
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     1
#!/usr/bin/env bash
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     2
#
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     3
# mirrors the Isabelle website
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     4
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     5
HOST=$(hostname)
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     6
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
     7
case ${HOST} in
68750
7087748996af updated common hosts;
wenzelm
parents: 54674
diff changeset
     8
  sunbroy* | atbroy* | macbroy* | lxbroy* | lxcisa*)
74916
79ceca45fcbc proper path;
wenzelm
parents: 68750
diff changeset
     9
    DEST=/p/home/isabelle/html-data/html-data
17671
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    10
    ;;
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    11
  *.cl.cam.ac.uk)
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    12
    USER=paulson
54636
cc126144f662 updated mirror script for Cambridge
paulson
parents: 51087
diff changeset
    13
    DEST=/anfs/bigdisc/lp15/Isabelle
17671
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    14
    ;;
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    15
  *)
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    16
    echo "Unknown destination directory for ${HOST}"
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    17
    exit 2
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    18
    ;;
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    19
esac
e9e341bc7d42 website preparation for Isabelle2005
haftmann
parents:
diff changeset
    20
25463
8b9c4582795a simplified website rsync
haftmann
parents: 18173
diff changeset
    21
exec $(dirname $0)/isasync $DEST