Admin/cvs-copy
author paulson
Tue, 10 Feb 2004 12:02:11 +0100
changeset 14378 69c4d5997669
parent 12721 226fc0e2e7e3
child 16279 4cc37b145b97
permissions -rwxr-xr-x
generic of_nat and of_int functions, and generalization of iszero and neg
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12721
226fc0e2e7e3 #!/usr/bin/env bash;
wenzelm
parents: 9796
diff changeset
     1
#!/usr/bin/env bash
9781
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
     2
#
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
     3
# $Id$
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
     4
#
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
     5
# cvs-copy - make copy of CVS controlled directory hierarchy
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
     6
#
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
     7
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
     8
## diagnostics
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
     9
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    10
PRG=$(basename "$0")
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    11
THIS=$(cd $(dirname "$0"); echo "$PWD")
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    12
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    13
function usage()
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    14
{
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    15
  echo
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    16
  echo "Usage: $PRG FROMDIR TODIR"
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    17
  echo
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    18
  echo "  Make copy of CVS controlled directory hierarchy"
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    19
  exit 1
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    20
}
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    21
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    22
function fail()
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    23
{
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    24
  echo "$1" >&2
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    25
  exit 2
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    26
}
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    27
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    28
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    29
## process command line
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    30
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    31
[ "$#" -ne 2 ] && usage
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    32
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    33
FROMDIR="$1"; shift
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    34
TODIR="$1"; shift
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    35
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    36
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    37
## main
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    38
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    39
function copy ()
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    40
{
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    41
  local PREFIX="$1"
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    42
  local TYPE NAME REST
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    43
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    44
  [ -d "$FROMDIR/${PREFIX}CVS" ] || fail "Bad CVS directory '$FROMDIR/${PREFIX}.'"
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    45
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    46
  { cat "$FROMDIR/${PREFIX}CVS/Entries" || \
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    47
    fail "Cannot read '$FROMDIR/${PREFIX}CVS/Entries'"; } | \
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    48
  {
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    49
    ORIG_IFS="$IFS"
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    50
    IFS="/"
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    51
    while read TYPE NAME REST
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    52
    do
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    53
      if [ -n "$NAME" ]; then
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    54
        if [ "$TYPE" = D ]; then
9796
wenzelm
parents: 9781
diff changeset
    55
          echo "X ${PREFIX}$NAME"
9781
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    56
          mkdir -p "$TODIR/${PREFIX}$NAME" || fail "Bad directory '$TODIR/${PREFIX}$NAME'"
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    57
          copy "${PREFIX}$NAME/" || return "$?"
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    58
        else
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    59
          { [ ! -d "$TODIR/${PREFIX}$NAME" ] && \
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    60
            cp -af "$FROMDIR/${PREFIX}$NAME" "$TODIR/${PREFIX}$NAME"; } || \
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    61
          fail "Cannot install '$TODIR/${PREFIX}$NAME'"
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    62
        fi
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    63
      fi
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    64
    done
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    65
    IFS="$ORIG_IFS"
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    66
  }
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    67
}
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    68
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    69
mkdir -p "$TODIR" || fail "Bad directory '$TODIR'"
32378f1c2f17 cvs-copy - make copy of CVS controlled directory hierarchy;
wenzelm
parents:
diff changeset
    70
copy ""