# HG changeset patch
# User wenzelm
# Date 1434718944 -7200
# Node ID a79f89a36dffc4a757464a73a9d2d4323f6c3f9f
# Parent  78a82c37b4b25de6f2da9affca220668a62c48b7
uniform system_mode for build test: avoid spurious output_dir/log that is not required later;

diff -r 78a82c37b4b2 -r a79f89a36dff src/Pure/Tools/build_console.scala
--- a/src/Pure/Tools/build_console.scala	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/Pure/Tools/build_console.scala	Fri Jun 19 15:02:24 2015 +0200
@@ -21,7 +21,7 @@
   {
     if (no_build ||
         Build.build(options = options, build_heap = true, no_build = true,
-          dirs = dirs, sessions = List(session)) == 0) 0
+          dirs = dirs, system_mode = system_mode, sessions = List(session)) == 0) 0
     else {
       progress.echo("Build started for Isabelle/" + session + " ...")
       Build.build(options = options, progress = progress, build_heap = true,
diff -r 78a82c37b4b2 -r a79f89a36dff src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Thu Jun 18 16:17:51 2015 +0200
+++ b/src/Pure/Tools/main.scala	Fri Jun 19 15:02:24 2015 +0200
@@ -47,7 +47,7 @@
             options.string("jedit_logic"))
 
           if (Build.build(options = options, build_heap = true, no_build = true,
-              dirs = dirs, sessions = List(session)) == 0)
+              dirs = dirs, system_mode = system_mode, sessions = List(session)) == 0)
             system_dialog.return_code(0)
           else {
             system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")")