# HG changeset patch
# User wenzelm
# Date 1626467561 -7200
# Node ID d609fa3e816d5fa6b727bfcf1dba0cbc2701f200
# Parent  19ad7a0999920d51ee386e143d58bde17e2ebe70
more robust;

diff -r 19ad7a099992 -r d609fa3e816d src/Tools/Setup/isabelle/setup/Build.java
--- a/src/Tools/Setup/isabelle/setup/Build.java	Fri Jul 16 22:27:00 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Build.java	Fri Jul 16 22:32:41 2021 +0200
@@ -283,6 +283,7 @@
         if (!java_sources.isEmpty()) {
             CharArrayWriter out = new CharArrayWriter();
             boolean ok = compiler.getTask(out, file_manager, null, options, null, java_sources).call();
+            out.flush();
             compiler_result(ok, out.toString(), "Java sources");
         }
     }