aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--toplevel/coqtop.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b196e6b4b8..ecd9cafaca 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -32,8 +32,8 @@ let get_version_date () =
let print_header () =
let (ver,rev) = (get_version_date ()) in
- pp (str "Welcome to Coq "++ str ver ++ str " (" ++ str rev ++ str ")" ++ fnl ());
- flush stdout
+ pp (str "Welcome to Coq "++ str ver ++ str " (" ++ str rev ++ str ")" ++ fnl ());
+ pp_flush ()
let output_context = ref false