quick fix to console.php: don't save blank lines into readline history

scripts/console.php

@@ -45,11 +45,13 @@ function read_input_line($prompt)
     if (CONSOLE_INTERACTIVE) {
         if (CONSOLE_READLINE) {
             $line = readline($prompt);
+            if (trim($line) != '') {
                 readline_add_history($line);
                 if (defined('CONSOLE_HISTORY')) {
                     // Save often; it's easy to hit fatal errors.
                     readline_write_history(CONSOLE_HISTORY);
                 }
+            }
             return $line;
         } else {
             return readline_emulation($prompt);