--- a/lib/Tools/changeparent Fri Apr 25 15:06:21 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-#!/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" >&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