| Index: tools/grokdump.py
|
| diff --git a/tools/grokdump.py b/tools/grokdump.py
|
| index 4525e7ef33e703974b8b610cdbd13c4a2c6668f4..c05c79ed3f0387ef8b22634ce5647efba374d5c9 100755
|
| --- a/tools/grokdump.py
|
| +++ b/tools/grokdump.py
|
| @@ -2045,7 +2045,7 @@ function onpage(kind, address) {
|
|
|
| <body>
|
| <div class="header">
|
| - <form class="navigation" action=/search.html">
|
| + <form class="navigation" action="search.html">
|
| <a href="summary.html?%(query_dump)s">Context info</a>
|
| <a href="info.html?%(query_dump)s">Dump info</a>
|
| <a href="modules.html?%(query_dump)s">Modules</a>
|
|
|