diff --git a/os/console.c b/os/console.c index d0d9484df..f1629c93c 100644 --- a/os/console.c +++ b/os/console.c @@ -235,6 +235,7 @@ int Yap_GetCharForSIGINT(void) { ; } LOCAL_newline = TRUE; + fflush(NULL); return ch; } diff --git a/os/readline.c b/os/readline.c index 291ae45d8..19717f715 100644 --- a/os/readline.c +++ b/os/readline.c @@ -458,6 +458,7 @@ int Yap_ReadlineForSIGINT(void) { ch = myrl_line[0]; free((void *)myrl_line); myrl_line = NULL; + fflush(NULL); return ch; } else { myrl_line = (const unsigned char *)readline("Action (h for help): "); @@ -468,6 +469,7 @@ int Yap_ReadlineForSIGINT(void) { ch = myrl_line[0]; free((void *)myrl_line); myrl_line = NULL; + fflush(NULL); return ch; } }