1 files changed, 11 insertions, 0 deletions
diff --git a/html/haddock.js b/html/haddock.js
new file mode 100644
index 00000000..4f6a2e44
--- /dev/null
+++ b/html/haddock.js
@@ -0,0 +1,11 @@
+// Haddock JavaScript utilities
+function toggle(button,id) {
+   var n = document.getElementById(id).style;
+   if (n.display == "none") {
+	button.childNodes[0].data = "-";
+	n.display = "inline";
+   } else {
+	button.childNodes[0].data = "+";
+	n.display = "none";
+   }
+}