-function manage_distro () {
-
- echo manage_distro disabled
-
-# both .mk and .xml inserted into princeton's cvs
-
-# DISTROFILE=$BUILD/$DISTRO.mk
-#
-# if [ -f $DISTROFILE ] ; then
-# echo Using $DISTROFILE
-# elif [ -f $ROOT/$DISTRO.mk ] ; then
-# echo Using $ROOT/$DISTRO.mk
-# ln -s $ROOT/$DISTRO.mk $DISTROFILE
-# else
-# echo Could not locate $DISTRO.mk
-# exit 1
-# fi
-#
-# if [ "$DISTRO" != planetlab ] ; then
-# DISTROFILE=$BUILD/$DISTRO.xml
-#
-# if [ -f $DISTROFILE ] ; then
-# echo Using $DISTROFILE
-# elif [ -f $ROOT/$DISTRO.xml ] ; then
-# echo Using $ROOT/$DISTRO.xml
-# ln -s $ROOT/$DISTRO.xml $DISTROFILE
-# else
-# echo Could not locate $DISTRO.xml
-# exit 1
-# fi
-# fi
-
-}
-