Mon Jan  9 18:04:38 CET 2006  Michal Sojka <sojkam1@fel.cvut.cz>
  * Deleted duplicated output from flexinode module.
diff -rN -u old-info/modules/flexinode/flexinode.module new-info/modules/flexinode/flexinode.module
--- old-info/modules/flexinode/flexinode.module	2006-01-09 18:09:19.722570965 +0100
+++ new-info/modules/flexinode/flexinode.module	2006-01-09 18:09:19.733569281 +0100
@@ -294,8 +294,6 @@
   else {
      $output .= theme('box', t('Your search yielded no results'), search_help('search#noresults'));
   }
-  $output .= theme('table', $header, $rows);
-  $output .= theme('pager', NULL, 20, 0, tablesort_pager());
 
   drupal_set_title(t('%type search results', array('%type' => t($ctype->name))));
   return $output;