-function manage_distro () {
-
-# 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
-
-}
-