Merge branch 'master' into jedi/dev

This commit is contained in:
/jedi/ 2018-12-30 12:01:55 +01:00
commit f949d07115
9 changed files with 68 additions and 68 deletions

View file

@ -76,7 +76,7 @@ function get_stats(){
if ($row = $res->fetch_assoc()) {
$ret["match"] = $row["c"];
}
$ret["unmatched"] = $ret["found"] + $ret["lost"] - 2 * $ret["match"];
return $ret;
}