no more php-5.3 deprecated stuff

[plewww.git] / planetlab / common / adminsearch.php

diff --git a/planetlab/common/adminsearch.php b/planetlab/common/adminsearch.php
index ee2da8f..3b02079 100644 (file)
--- a/planetlab/common/adminsearch.php
+++ b/planetlab/common/adminsearch.php
@@ -34,7 +34,7 @@ $pattern="";
 if (isset($_GET['pattern'])) { $pattern=$_GET['pattern']; }
 if (isset($_POST['pattern'])) { $pattern=$_POST['pattern']; }
 
-$tokens=split(" ",$pattern);
+$tokens=explode(" ",$pattern);
 function token_filter ($t) { $t = trim($t); if (empty($t)) return false; return true; }
 $tokens=array_filter($tokens, "token_filter");