author | wenzelm |
Wed, 04 Dec 1996 13:10:11 +0100 | |
changeset 2310 | f49958ca2f8d |
parent 2309 | 390c1b6baaa5 |
child 2311 | 69c51db9481f |
--- a/lib/Tools/changeparent Wed Dec 04 13:08:40 1996 +0100 +++ b/lib/Tools/changeparent Wed Dec 04 13:10:11 1996 +0100 @@ -1,7 +1,9 @@ #!/bin/bash # +# $Id$ +# # DESCRIPTION: change parent of Poly/ML database -# + PRG=$(basename $0) @@ -32,7 +34,7 @@ case "$ML_SYSTEM" in polyml-*) [ ! -w "$DB" ] && fail "Database not writable: $DB" - $POLYML_HOME/changeParent "$DB" "$PARENT" + $ML_HOME/changeParent "$DB" "$PARENT" ;; *) fail "You're not set up for Poly/ML!"