lib/Tools/changeparent
author wenzelm
Fri, 07 Mar 1997 11:48:46 +0100
changeset 2754 59bd96046ad6
parent 2334 00db792beb4e
child 3007 e5efa177ee0c
permissions -rwxr-xr-x
moved settings comment to build;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2334
00db792beb4e added -norc option;
wenzelm
parents: 2310
diff changeset
     1
#!/bin/bash -norc
2295
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
     2
#
2310
f49958ca2f8d fixed ML_HOME;
wenzelm
parents: 2295
diff changeset
     3
# $Id$
f49958ca2f8d fixed ML_HOME;
wenzelm
parents: 2295
diff changeset
     4
#
2295
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: change parent of Poly/ML database
2310
f49958ca2f8d fixed ML_HOME;
wenzelm
parents: 2295
diff changeset
     6
2295
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
     7
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
     8
PRG=$(basename $0)
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
     9
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    10
function usage()
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    11
{
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    12
  echo
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    13
  echo "Usage: $PRG DB PARENT"
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    14
  echo
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    15
  echo "  Change parent of Poly/ML database DB to PARENT (full path name!)."
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    16
  echo
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    17
  exit 1
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    18
}
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    19
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    20
function fail()
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    21
{
2334
00db792beb4e added -norc option;
wenzelm
parents: 2310
diff changeset
    22
  echo "$1" >&2
2295
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    23
  exit 2
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    24
}
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    25
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    26
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    27
## main
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    28
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    29
[ $# -ne 2 ] && usage
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    30
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    31
DB="$1"
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    32
PARENT="$2"
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    33
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    34
case "$ML_SYSTEM" in
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    35
  polyml-*)
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    36
    [ ! -w "$DB" ] && fail "Database not writable: $DB"
2310
f49958ca2f8d fixed ML_HOME;
wenzelm
parents: 2295
diff changeset
    37
    $ML_HOME/changeParent "$DB" "$PARENT"
2295
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    38
    ;;
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    39
  *)
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    40
    fail "You're not set up for Poly/ML!"
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    41
    ;;
bae5683c2891 changeparent: change parent of Poly/ML database.
wenzelm
parents:
diff changeset
    42
esac