From 5403a5af081b01916e1d94403f608051c377ee7f Mon Sep 17 00:00:00 2001
From: Simon Marlow <simonmar@microsoft.com>
Date: Wed, 11 Oct 2006 14:17:37 +0000
Subject: 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.

---
 html/haddock-util.js | 15 +++++++++++++++
 html/haddock.js      | 15 ---------------
 2 files changed, 15 insertions(+), 15 deletions(-)
 create mode 100644 html/haddock-util.js
 delete mode 100644 html/haddock.js

(limited to 'html')

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";
+   }
+}
diff --git a/html/haddock.js b/html/haddock.js
deleted file mode 100644
index 4280d19c..00000000
--- a/html/haddock.js
+++ /dev/null
@@ -1,15 +0,0 @@
-// 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";
-   }
-}
-- 
cgit v1.2.3