# HG changeset patch
# User ymh <ymh.work@gmail.com>
# Date 1479137257 -3600
# Node ID 6eb84397be156cddb50d4685b113c82527ab5ea2
# Parent  3fbc9b47957839324dae9d533cab816552852640
Correct error message 'split is deprecated' in php

diff -r 3fbc9b479578 -r 6eb84397be15 server/src/app/Libraries/Filters/CorpusFilterManager.php
--- a/server/src/app/Libraries/Filters/CorpusFilterManager.php	Mon Nov 14 15:39:05 2016 +0100
+++ b/server/src/app/Libraries/Filters/CorpusFilterManager.php	Mon Nov 14 16:27:37 2016 +0100
@@ -16,7 +16,7 @@
         }
 
         if(is_string($ids)) {
-            return split(",", $ids);
+            return explode(",", $ids);
         }
         else return $ids;
     }