diff options
Diffstat (limited to 'html')
| -rw-r--r-- | html/haddock.css | 3 | ||||
| -rw-r--r-- | html/haddock.js | 4 | ||||
| -rw-r--r-- | html/minus.jpg | bin | 0 -> 1271 bytes | |||
| -rw-r--r-- | html/plus.jpg | bin | 0 -> 1512 bytes |
4 files changed, 4 insertions, 3 deletions
diff --git a/html/haddock.css b/html/haddock.css index b853bf76..1807a26e 100644 --- a/html/haddock.css +++ b/html/haddock.css @@ -35,7 +35,8 @@ TD.s15 { height: 15px; } SPAN.keyword { text-decoration: underline; } -BUTTON.coll { width : 2em; } +/* Resize the buttom image to match the text size */ +IMG.coll { width : 1em; height: 1em; } /* --------- Documentation elements ---------- */ diff --git a/html/haddock.js b/html/haddock.js index 4f6a2e44..8dbd0a03 100644 --- a/html/haddock.js +++ b/html/haddock.js @@ -2,10 +2,10 @@ function toggle(button,id) { var n = document.getElementById(id).style; if (n.display == "none") { - button.childNodes[0].data = "-"; + button.src = "minus.jpg"; n.display = "inline"; } else { - button.childNodes[0].data = "+"; + button.src = "plus.jpg"; n.display = "none"; } } diff --git a/html/minus.jpg b/html/minus.jpg Binary files differnew file mode 100644 index 00000000..d3fb7e32 --- /dev/null +++ b/html/minus.jpg diff --git a/html/plus.jpg b/html/plus.jpg Binary files differnew file mode 100644 index 00000000..c6b6350f --- /dev/null +++ b/html/plus.jpg |
