planetlab/nodes/production_hosts.php

   1 <?php
   2 header("Content-type: text/plain");
   3 $which_node_list= "production_hosts";
   4 include('_gen_node_lists.php');
   5 ?>