From 08b9953dfe457e36a9ee3343bc0c42b744a62446 Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Sun, 29 Oct 2023 17:32:10 +0000
Subject: [PATCH] Flush stdout after outputting debug message

TextIO.output() doesn't flush stdout, but print() does. Flushing is
necessary to make sure the messages are printed in a timely fashion,
which is important when debugging timing/performance issues.

The performance hit of the extra flushing should be negligible, as
even when these debug messages are enabled, they are only printed a
few dozen times or so.
---
 tools-poly/poly/poly-init2.ML | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools-poly/poly/poly-init2.ML b/tools-poly/poly/poly-init2.ML
index 520023b1f1..0f64c64515 100644
--- a/tools-poly/poly/poly-init2.ML
+++ b/tools-poly/poly/poly-init2.ML
@@ -32,7 +32,7 @@ local
   val meta_debug = ref false
 
   fun MDBG s = if !meta_debug then
-                 TextIO.output(TextIO.stdOut, "META_DEBUG: " ^ s() ^ "\n")
+                 TextIO.print("META_DEBUG: " ^ s() ^ "\n")
                else ()
 
   infix ++