Grrr! Nico.

diff --git a/lib/deprecatedlib.php b/lib/deprecatedlib.php
index e8b96db743b984e324e03d6450d9763e85581cc2..bba4202d42fcd888071c6ed49b0004d01418d1d5 100644 (file)
--- 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();
     }
-
 }