Rename haddock.js to haddock-util.js

haddock.js will be run automatically by Windows when you type
'haddock' if it is found on the PATH, so rename to avoid confusion.
Spotted by Adrian Hey.

1 files changed, 15 insertions, 0 deletions

diff --git a/html/haddock-util.js b/html/haddock-util.js
new file mode 100644
index 00000000..4280d19c
--- /dev/null
+++ b/html/haddock-util.js
@@ -0,0 +1,15 @@
+// Haddock JavaScript utilities
+function toggle(button,id)
+{
+   var n = document.getElementById(id).style;
+   if (n.display == "none")
+   {
+	button.src = "minus.gif";
+	n.display = "block";
+   }
+   else
+   {
+	button.src = "plus.gif";
+	n.display = "none";
+   }
+}