# HG changeset patch
# User wenzelm
# Date 861973705 -7200
# Node ID db72904b42fb76657261e2a89a5b1056b8441f87
# Parent  b7922b9d7acd855b2e62c44988b5b97bdeae7077
obsolete;

diff -r b7922b9d7acd -r db72904b42fb lib/Tools/changeparent
--- 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