equal
deleted
inserted
replaced
48 |
48 |
49 if (Build.build(options = options, build_heap = true, no_build = true, |
49 if (Build.build(options = options, build_heap = true, no_build = true, |
50 dirs = dirs, system_mode = system_mode, sessions = List(session)) == 0) |
50 dirs = dirs, system_mode = system_mode, sessions = List(session)) == 0) |
51 system_dialog.return_code(0) |
51 system_dialog.return_code(0) |
52 else { |
52 else { |
53 system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")") |
53 system_dialog.title("Isabelle build (" + |
|
54 Isabelle_System.getenv("ML_IDENTIFIER") + " / " + |
|
55 "jdk-" + Platform.jvm_version + "-" + |
|
56 Isabelle_System.getenv("ISABELLE_JAVA_PLATFORM") + ")") |
54 system_dialog.echo("Build started for Isabelle/" + session + " ...") |
57 system_dialog.echo("Build started for Isabelle/" + session + " ...") |
55 |
58 |
56 val (out, rc) = |
59 val (out, rc) = |
57 try { |
60 try { |
58 ("", |
61 ("", |