Admin/cvs-copy
author huffman
Tue Jul 12 18:26:44 2005 +0200 (2005-07-12)
changeset 16777 555c8951f05c
parent 16280 d7f8c48d5acb
permissions -rwxr-xr-x
added lemmas sfst_defined_iff, ssnd_defined_iff, sfst_defined, ssnd_defined
wenzelm@12721
     1
#!/usr/bin/env bash
wenzelm@9781
     2
#
wenzelm@9781
     3
# $Id$
wenzelm@9781
     4
#
wenzelm@9781
     5
# cvs-copy - make copy of CVS controlled directory hierarchy
wenzelm@9781
     6
#
wenzelm@9781
     7
wenzelm@9781
     8
## diagnostics
wenzelm@9781
     9
wenzelm@9781
    10
PRG=$(basename "$0")
wenzelm@9781
    11
THIS=$(cd $(dirname "$0"); echo "$PWD")
wenzelm@9781
    12
wenzelm@9781
    13
function usage()
wenzelm@9781
    14
{
wenzelm@9781
    15
  echo
wenzelm@9781
    16
  echo "Usage: $PRG FROMDIR TODIR"
wenzelm@9781
    17
  echo
wenzelm@9781
    18
  echo "  Make copy of CVS controlled directory hierarchy"
wenzelm@9781
    19
  exit 1
wenzelm@9781
    20
}
wenzelm@9781
    21
wenzelm@9781
    22
function fail()
wenzelm@9781
    23
{
wenzelm@9781
    24
  echo "$1" >&2
wenzelm@9781
    25
  exit 2
wenzelm@9781
    26
}
wenzelm@9781
    27
wenzelm@9781
    28
wenzelm@9781
    29
## process command line
wenzelm@9781
    30
wenzelm@9781
    31
[ "$#" -ne 2 ] && usage
wenzelm@9781
    32
wenzelm@9781
    33
FROMDIR="$1"; shift
wenzelm@9781
    34
TODIR="$1"; shift
wenzelm@9781
    35
wenzelm@9781
    36
haftmann@16279
    37
## GNU cp required
haftmann@16279
    38
haftmann@16279
    39
CP=cp
haftmann@16279
    40
type -path gcp >/dev/null && CP=gcp
haftmann@16279
    41
haftmann@16279
    42
wenzelm@9781
    43
## main
wenzelm@9781
    44
wenzelm@9781
    45
function copy ()
wenzelm@9781
    46
{
wenzelm@9781
    47
  local PREFIX="$1"
wenzelm@9781
    48
  local TYPE NAME REST
wenzelm@9781
    49
wenzelm@9781
    50
  [ -d "$FROMDIR/${PREFIX}CVS" ] || fail "Bad CVS directory '$FROMDIR/${PREFIX}.'"
wenzelm@9781
    51
wenzelm@9781
    52
  { cat "$FROMDIR/${PREFIX}CVS/Entries" || \
wenzelm@9781
    53
    fail "Cannot read '$FROMDIR/${PREFIX}CVS/Entries'"; } | \
wenzelm@9781
    54
  {
wenzelm@9781
    55
    ORIG_IFS="$IFS"
wenzelm@9781
    56
    IFS="/"
wenzelm@9781
    57
    while read TYPE NAME REST
wenzelm@9781
    58
    do
wenzelm@9781
    59
      if [ -n "$NAME" ]; then
wenzelm@9781
    60
        if [ "$TYPE" = D ]; then
wenzelm@9796
    61
          echo "X ${PREFIX}$NAME"
wenzelm@9781
    62
          mkdir -p "$TODIR/${PREFIX}$NAME" || fail "Bad directory '$TODIR/${PREFIX}$NAME'"
wenzelm@9781
    63
          copy "${PREFIX}$NAME/" || return "$?"
wenzelm@9781
    64
        else
wenzelm@9781
    65
          { [ ! -d "$TODIR/${PREFIX}$NAME" ] && \
haftmann@16280
    66
            $CP -af "$FROMDIR/${PREFIX}$NAME" "$TODIR/${PREFIX}$NAME"; } || \
wenzelm@9781
    67
          fail "Cannot install '$TODIR/${PREFIX}$NAME'"
wenzelm@9781
    68
        fi
wenzelm@9781
    69
      fi
wenzelm@9781
    70
    done
wenzelm@9781
    71
    IFS="$ORIG_IFS"
wenzelm@9781
    72
  }
wenzelm@9781
    73
}
wenzelm@9781
    74
wenzelm@9781
    75
mkdir -p "$TODIR" || fail "Bad directory '$TODIR'"
wenzelm@9781
    76
copy ""