Search failed with postgresql

Search returns no result. Postgresql logs contains :

ERROR: operator does not exist: integer || integer at character 153

I trace this back in node.module on line 1238 :

$ranking[] = '%d * POW(2, (GREATEST(MAX(n.created), MAX(n.changed), MAX(c.last_comment_timestamp) || 1) - %d) * 6.43e-8)';

I suggest :

if($GLOBALS['db_type']=='pgsql') {
$ranking[] = '%d * POW(2, (GREATEST(MAX(n.created), MAX(n.changed), MAX(c.last_comment_timestamp) # 1) - %d) * 6.43e-8)';
} else {
$ranking[] = '%d * POW(2, (GREATEST(MAX(n.created), MAX(n.changed), MAX(c.last_comment_timestamp) || 1) - %d) * 6.43e-8)';
}