author | wenzelm |
Wed, 04 Dec 1996 13:18:26 +0100 | |
changeset 2314 | 67bf78c7c725 |
parent 2310 | f49958ca2f8d |
child 2334 | 00db792beb4e |
permissions | -rwxr-xr-x |
#!/bin/bash # # $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" 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