# HG changeset patch
# User wenzelm
# Date 1570371920 -7200
# Node ID 02edce6f0c71a8a8e7509afa0a4dc86ae1ab88dd
# Parent  73514ccad7a61a18909c632f0778ba86c864f561
clarified signature: more options;

diff -r 73514ccad7a6 -r 02edce6f0c71 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Oct 06 16:22:43 2019 +0200
+++ b/src/Pure/Tools/build.scala	Sun Oct 06 16:25:20 2019 +0200
@@ -858,15 +858,16 @@
     progress: Progress = No_Progress,
     build_heap: Boolean = false,
     dirs: List[Path] = Nil,
+    fresh: Boolean = false,
     strict: Boolean = false): Int =
   {
     val rc =
-      if (build(options, build_heap = build_heap, no_build = true, dirs = dirs,
+      if (!fresh && build(options, build_heap = build_heap, no_build = true, dirs = dirs,
           sessions = List(logic)).ok) 0
       else {
         progress.echo("Build started for Isabelle/" + logic + " ...")
-        Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
-          sessions = List(logic)).rc
+        Build.build(options, progress = progress, build_heap = build_heap, fresh_build = fresh,
+          dirs = dirs, sessions = List(logic)).rc
       }
 
     if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc