35 |
<script type="text/javascript"> |
<script type="text/javascript"> |
36 |
document.write("<input name=\"query\" value=\""); |
document.write("<input name=\"query\" value=\""); |
37 |
|
|
38 |
if(args.query) |
if (args.query) { |
|
{ |
|
39 |
var search_string = args.query.replace(/\+/gi," "); |
var search_string = args.query.replace(/\+/gi," "); |
40 |
document.write(search_string); |
document.write(search_string); |
41 |
} |
} |
48 |
|
|
49 |
<script type="text/javascript"> |
<script type="text/javascript"> |
50 |
|
|
51 |
if (args.query) |
if (args.query) { |
|
{ |
|
52 |
document.write("<div id=\"results\"><h2>Please wait...</h2></div>\n"); |
document.write("<div id=\"results\"><h2>Please wait...</h2></div>\n"); |
53 |
doSearch(args.index_name, args.query, printResults); |
doSearch(args.index_name, args.query, printResults); |
54 |
} |
} |