tuned;
authorwenzelm
Thu Mar 09 17:25:28 2000 +0100 (2000-03-09)
changeset 8397f2d371bde3c4
parent 8396 16f6de8c897b
child 8398 f1c80ed70f48
tuned;
Admin/mirror-dist
Admin/mirror-isabelle-dist
     1.1 --- a/Admin/mirror-dist	Thu Mar 09 17:19:49 2000 +0100
     1.2 +++ b/Admin/mirror-dist	Thu Mar 09 17:25:28 2000 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  HOST=$(hostname)
     1.5  
     1.6  case  ${HOST} in
     1.7 -  sunbroy79)
     1.8 +  sunbroy*)
     1.9      #test
    1.10      DEST=/tmp/isabelle-dist
    1.11      mkdir -p $DEST
    1.12 @@ -20,4 +20,4 @@
    1.13      ;;
    1.14  esac
    1.15  
    1.16 -mirror-isabelle-dist -d $DEST
    1.17 +exec $(dirname $0)/mirror-isabelle-dist -d $DEST
     2.1 --- a/Admin/mirror-isabelle-dist	Thu Mar 09 17:19:49 2000 +0100
     2.2 +++ b/Admin/mirror-isabelle-dist	Thu Mar 09 17:25:28 2000 +0100
     2.3 @@ -5,23 +5,10 @@
     2.4  # $Id$
     2.5  #
     2.6  
     2.7 -
     2.8 -
     2.9 -## self references
    2.10 +## diagnostics
    2.11  
    2.12  PRG=`basename "$0"`
    2.13  
    2.14 -if [ -h "$0" ]; then
    2.15 -  THIS=`cd \`dirname "$0"\`; cd \`dirname \\\`find "$0" -ls | cut -d ">" -f 2\\\`\`; pwd`
    2.16 -else
    2.17 -  THIS=`cd \`dirname "$0"\`; pwd`
    2.18 -fi
    2.19 -
    2.20 -SUPER=`cd "$THIS/.."; pwd`
    2.21 -
    2.22 -
    2.23 -## diagnostics
    2.24 -
    2.25  usage()
    2.26  {
    2.27    echo
    2.28 @@ -29,7 +16,7 @@
    2.29    echo
    2.30    echo "  Options are:"
    2.31    echo "    -n    dry run, don't do anything, just report what would happen"
    2.32 -  echo "    -d    delete files that are not on the server"
    2.33 +  echo "    -d    delete files that are not on the server (beware!)"
    2.34    echo
    2.35    exit 1
    2.36  }
    2.37 @@ -71,6 +58,7 @@
    2.38  
    2.39  DEST="$1"; shift;
    2.40  
    2.41 +
    2.42  ## main
    2.43  
    2.44 -rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. $DEST/.
    2.45 \ No newline at end of file
    2.46 +exec rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/."