# HG changeset patch
# User wenzelm
# Date 849547168 -3600
# Node ID bae5683c2891b927548186e8848edbe4a2db8201
# Parent  a67343c87db47a92cd7563553c77a6c704fd73b8
changeparent: change parent of Poly/ML database.

diff -r a67343c87db4 -r bae5683c2891 lib/Tools/changeparent
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/changeparent	Mon Dec 02 18:19:28 1996 +0100
@@ -0,0 +1,40 @@
+#!/bin/bash
+#
+# 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"
+    $POLYML_HOME/changeParent "$DB" "$PARENT"
+    ;;
+  *)
+    fail "You're not set up for Poly/ML!"
+    ;;
+esac