replace function deprecated in php 5.3

fantu

2008-12-23 043a0a320744d0f5f4214898210edd8a907b8030

 interface/web/admin/dbsync_del.php

@@ -39,11 +39,7 @@
* End Form configuration
******************************************/

// Checke Berechtigungen für Modul
if(!stristr($_SESSION["s"]["user"]["modules"],$_SESSION["s"]["module"]["name"])) {
   header("Location: ../index.php");
   exit;
}
$app->auth->check_module_permissions('admin');

include_once($list_def_file);