flush

josephnunn · May 16, 2016 · f54e11d · f54e11d
1 parent 9f2ba2d
commit f54e11d
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 0 deletions.
diff --git 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
@@ -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;
     }
   }
-Original file line number
+Diff line change
@@ Expand Up / @@ -235,6 +235,7 @@ int Yap_GetCharForSIGINT(void) { @@
           ;
       }
       LOCAL_newline = TRUE;
+      fflush(NULL);
       return ch;
     }
@@ Expand Down @@