diff --git a/lib/deprecatedlib.php b/lib/deprecatedlib.php index e8b96db743b..bba4202d42f 100644 --- a/lib/deprecatedlib.php +++ b/lib/deprecatedlib.php @@ -3043,7 +3043,5 @@ function choose_from_menu ($options, $name, $selected='', $nothing='choose', $sc return $output; } else { echo $output; - die(); } - }