src/Pure/ML/ml_console.scala
changeset 67846 bdf6933f7ac9
parent 67808 9cb7f5f0bf41
child 68209 aeffd8f1f079
--- a/src/Pure/ML/ml_console.scala	Tue Mar 13 17:15:01 2018 +0100
+++ b/src/Pure/ML/ml_console.scala	Tue Mar 13 18:28:12 2018 +0100
@@ -52,14 +52,14 @@
 
       // build
       if (!no_build && !raw_ml_system &&
-          !Build.build(options = options, build_heap = true, no_build = true,
+          !Build.build(options, build_heap = true, no_build = true,
             dirs = dirs, system_mode = system_mode, sessions = List(logic)).ok)
       {
         val progress = new Console_Progress()
         progress.echo("Build started for Isabelle/" + logic + " ...")
         progress.interrupt_handler {
           val res =
-            Build.build(options = options, progress = progress, build_heap = true,
+            Build.build(options, progress = progress, build_heap = true,
               dirs = dirs, system_mode = system_mode, sessions = List(logic))
           if (!res.ok) sys.exit(res.rc)
         }