add an extra 0 for initial prompt

HOL-Theorem-Prover · Sep 24, 2024 · 42fc32e · 42fc32e
1 parent 57c37f8
commit 42fc32e
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/tools-poly/holrepl.ML b/tools-poly/holrepl.ML
@@ -133,6 +133,10 @@ fun topLevel diag {nameSpace, exitLoop, exitOnError, isInteractive, zeroTerm,
       if zeroTerm then
         let
           val endOfCommand = ref false;
+
+          (* Initial prompt / end of splash message *)
+          val () = printOut "\000";
+
           (* Each character typed is fed into the compiler but a "\0"
              terminates the input. *)
           fun readin () =