+ repetitions when the user enters an empty line. */
+
+static char *saved_command_line;
+
+/* If not NULL, the arguments that should be passed if
+ saved_command_line is repeated. */
+
+static const char *repeat_arguments;
+
+/* The previous last command line executed on the console. Used for command
+ repetitions when a command wants to relaunch the previously launched
+ command. We need this as when a command is running, saved_command_line
+ already contains the line of the currently executing command. */
+
+char *previous_saved_command_line;
+
+/* If not NULL, the arguments that should be passed if the
+ previous_saved_command_line is repeated. */
+
+static const char *previous_repeat_arguments;