diff options
| -rw-r--r-- | haddock-api/resources/html/haddock-util.js | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/haddock-api/resources/html/haddock-util.js b/haddock-api/resources/html/haddock-util.js index ba574356..fc7743fe 100644 --- a/haddock-api/resources/html/haddock-util.js +++ b/haddock-api/resources/html/haddock-util.js @@ -229,7 +229,7 @@ function perform_search(full) } function setSynopsis(filename) { - if (parent.window.synopsis) { + if (parent.window.synopsis && parent.window.synopsis.location) { if (parent.window.synopsis.location.replace) { // In Firefox this avoids adding the change to the history. parent.window.synopsis.location.replace(filename); |