+++ /dev/null
-
-function expand_source(node)
-{
- var text = $(node).text();
- var new_text;
- var new_display;
-
- if (text == "+") {
- new_text = "-";
- new_display = "block";
- } else {
- new_text = "+";
- new_display = "none";
- }
-
- $(node).text(new_text);
- $(node).parent().find("pre[class='source']").
- css("display", new_display);
-}