From e25eb941945b413904abd362329cf6c8220ba231 Mon Sep 17 00:00:00 2001 From: Robbert van Renesse Date: Tue, 26 Dec 2023 20:47:23 -0500 Subject: [PATCH] Fixed flush upon exit bug --- harmony_model_checker/main.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/harmony_model_checker/main.py b/harmony_model_checker/main.py index 03741e7e..a978f939 100644 --- a/harmony_model_checker/main.py +++ b/harmony_model_checker/main.py @@ -171,7 +171,10 @@ def handle_hco(ns, output_files): print("open " + url + " for detailed information, or use the HarmonyGUI", file=sys.stderr) if not disable_browser: webbrowser.open(url) - os._exit(0) # exit as minify may still be running + # exit as minify may still be running + print(flush=True) + print(file=sys.stderr, flush=True) + os._exit(0) def handle_version(_: argparse.Namespace): print("Version:", harmony_model_checker.__package__,