diff options
| -rw-r--r-- | html/haddock-util.js | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/html/haddock-util.js b/html/haddock-util.js index 5978f056..4a7e4255 100644 --- a/html/haddock-util.js +++ b/html/haddock-util.js @@ -198,7 +198,12 @@ function perform_search(full) function setSynopsis(filename) { if (parent.window.synopsis) { - parent.window.synopsis.location = filename; + if (parent.window.synopsis.location.replace) { + // In Firefox this avoids adding the change to the history. + parent.window.synopsis.location.replace(filename); + } else { + parent.window.synopsis.location = filename; + } } } |