svn:keywords

[nodeconfig.git] / PlanetLabConf / myplc.repo.php

diff --git a/PlanetLabConf/myplc.repo.php b/PlanetLabConf/myplc.repo.php
index b0d2960..f00f620 100644 (file)
--- a/PlanetLabConf/myplc.repo.php
+++ b/PlanetLabConf/myplc.repo.php
@@ -5,7 +5,7 @@
 // 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
@@ -84,6 +84,8 @@ if ( ! $repo) {
 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;