lib/Tools/changeparent
author wenzelm
Tue, 11 Mar 1997 13:05:40 +0100
changeset 2781 0d6fcae3ae45
parent 2334 00db792beb4e
child 3007 e5efa177ee0c
permissions -rwxr-xr-x
added THIS_IS_ISABELLE_BUILD;

#!/bin/bash -norc
#
# $Id$
#
# DESCRIPTION: change parent of Poly/ML database


PRG=$(basename $0)

function usage()
{
  echo
  echo "Usage: $PRG DB PARENT"
  echo
  echo "  Change parent of Poly/ML database DB to PARENT (full path name!)."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## main

[ $# -ne 2 ] && usage

DB="$1"
PARENT="$2"

case "$ML_SYSTEM" in
  polyml-*)
    [ ! -w "$DB" ] && fail "Database not writable: $DB"
    $ML_HOME/changeParent "$DB" "$PARENT"
    ;;
  *)
    fail "You're not set up for Poly/ML!"
    ;;
esac