// Thierry Parmentelat
// Copyright (C) 2008 INRIA
//
-// $Id: yum.conf.php 9688 2008-06-25 08:24:27Z thierry $
+// $Id$
//
// For PLC_NAME and PLC_BOOT_HOST
if ( ! $repo) {
echo "# WARNING: could not find a decent planetlab repo for this node\n";
$repo = array ($pldistro, "planetlab", "default probably wrong");
+ # don't define the repo in this case
+ exit;
}
list( $id, $dir, $name) = $repo;