diff --git a/src/streams.c b/src/streams.c index 02b0d1aeaeb..b41fada35eb 100644 --- a/src/streams.c +++ b/src/streams.c @@ -407,8 +407,13 @@ Int READ_GAP_ROOT ( const Char * filename ) if (OpenInput(&input, path)) { while (1) { ExecStatus status = ReadEvalCommand(0, &input, 0, 0); - if (STATE(UserHasQuit) || STATE(UserHasQUIT)) + if (STATE(UserHasQuit)) { + FlushRestOfInputLine(&input); + STATE(UserHasQuit) = FALSE; + } + else if (STATE(UserHasQUIT)) { break; + } if (status == STATUS_RETURN) { Pr("'return' must not be used in file", 0, 0); }