# HG changeset patch # User wenzelm # Date 1592590500 -7200 # Node ID 65ad3a6cee815b0c719caddf4036f8cd0e00302d # Parent 235173749448f3700ad3447026d63c47134ee366 tuned --- avoid error in IntelliJ IDEA; diff -r 235173749448 -r 65ad3a6cee81 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Fri Jun 19 18:44:36 2020 +0200 +++ b/src/Pure/Admin/build_history.scala Fri Jun 19 20:15:00 2020 +0200 @@ -240,11 +240,14 @@ val build_start = Date.now() val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args - val build_result = + + val build_isabelle = Other_Isabelle(root, isabelle_identifier = isabelle_identifier, - user_home = user_home, progress = build_out_progress)( - "build " + Bash.strings(build_args1 ::: afp_sessions), redirect = true, echo = true, - strict = false) + user_home = user_home, progress = build_out_progress) + val build_result = + build_isabelle("build " + Bash.strings(build_args1 ::: afp_sessions), + redirect = true, echo = true, strict = false) + val build_end = Date.now() val build_info: Build_Log.Build_Info =