aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--html/haddock-util.js7
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;
+ }
}
}