-/* $Id: search.js,v 1.16 2007-01-10 13:28:09 sondberg Exp $
+/* $Id: search.js,v 1.18 2007-01-11 10:18:38 sondberg Exp $
* ---------------------------------------------------
* Javascript container
*/
var p = off / max + 1;
var page_elem = create_element('a', p);
- var newline_node = document.createTextNode('\n');
+ var newline_node = document.createTextNode(' ');
if ((offset >= off) && (offset < (off + max))) {
page_elem.className = 'select';
function update_offset (offset) {
+ clearTimeout(searchtimer);
document.search.startrec.value = offset;
update_action('page');
check_search();