1 files changed, 6 insertions, 0 deletions
diff --git a/html/haddock-util.js b/html/haddock-util.js
index e5d6977e..364081f0 100644
--- a/html/haddock-util.js
+++ b/html/haddock-util.js
@@ -131,3 +131,9 @@ function perform_search(full)
         return ""; // should never be reached
     }
 }
+
+function setSynopsis(filename) {
+    if (parent.window.synopsis) {
+      parent.window.synopsis.location = filename;
+    }
+}