changeparent: change parent of Poly/ML database.
--- /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