obsolete;

--- a/Admin/MIRRORS	Wed Sep 21 18:35:31 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-
-* Cambridge (UK)
-http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/
-
-* Munich (Germany)
-http://isabelle.in.tum.de/dist/
-
-* New Jersey (USA)
-http://ftp.research.bell-labs.com/dist/smlnj/isabelle/source.html
-Dave MacQueen <[e-mail]>

--- a/Admin/cvs-copy	Wed Sep 21 18:35:31 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-#
-# cvs-copy - make copy of CVS controlled directory hierarchy
-#
-
-## diagnostics
-
-PRG=$(basename "$0")
-THIS=$(cd $(dirname "$0"); echo "$PWD")
-
-function usage()
-{
-  echo
-  echo "Usage: $PRG FROMDIR TODIR"
-  echo
-  echo "  Make copy of CVS controlled directory hierarchy"
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-[ "$#" -ne 2 ] && usage
-
-FROMDIR="$1"; shift
-TODIR="$1"; shift
-
-
-## GNU cp required
-
-CP=cp
-type -path gcp >/dev/null && CP=gcp
-
-
-## main
-
-function copy ()
-{
-  local PREFIX="$1"
-  local TYPE NAME REST
-
-  [ -d "$FROMDIR/${PREFIX}CVS" ] || fail "Bad CVS directory '$FROMDIR/${PREFIX}.'"
-
-  { cat "$FROMDIR/${PREFIX}CVS/Entries" || \
-    fail "Cannot read '$FROMDIR/${PREFIX}CVS/Entries'"; } | \
-  {
-    ORIG_IFS="$IFS"
-    IFS="/"
-    while read TYPE NAME REST
-    do
-      if [ -n "$NAME" ]; then
-        if [ "$TYPE" = D ]; then
-          echo "X ${PREFIX}$NAME"
-          mkdir -p "$TODIR/${PREFIX}$NAME" || fail "Bad directory '$TODIR/${PREFIX}$NAME'"
-          copy "${PREFIX}$NAME/" || return "$?"
-        else
-          { [ ! -d "$TODIR/${PREFIX}$NAME" ] && \
-            $CP -af "$FROMDIR/${PREFIX}$NAME" "$TODIR/${PREFIX}$NAME"; } || \
-          fail "Cannot install '$TODIR/${PREFIX}$NAME'"
-        fi
-      fi
-    done
-    IFS="$ORIG_IFS"
-  }
-}
-
-mkdir -p "$TODIR" || fail "Bad directory '$TODIR'"
-copy ""