diff --git a/lib/weblib.php b/lib/weblib.php index 81b386be0fb..2ad2651fbb1 100644 --- a/lib/weblib.php +++ b/lib/weblib.php @@ -804,8 +804,8 @@ function print_simple_box_end() { echo ""; } -function print_single_button($link, $options, $label="OK") { - echo "