# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1476803124 -3600
# Node ID 4750673a96da532052099a31d0bdb9c8b1213d15
# Parent  d85d887227457b048c4211df41c9aa73ee2698c9# Parent  b2f7aa1c6b75be23a197d2133c8704286a359e3f
Merge

diff -r d85d88722745 -r 4750673a96da src/Pure/Admin/ci_profile.scala
--- a/src/Pure/Admin/ci_profile.scala	Tue Oct 18 15:55:53 2016 +0100
+++ b/src/Pure/Admin/ci_profile.scala	Tue Oct 18 16:05:24 2016 +0100
@@ -22,12 +22,12 @@
       Build.build_selection(
         options = options,
         progress = progress,
-        clean_build = true,
+        clean_build = clean,
         verbose = true,
         max_jobs = jobs,
         dirs = include,
         select_dirs = select,
-        system_mode = false,
+        system_mode = true,
         selection = select_sessions _)
     }
     val end_time = Time.now()
@@ -136,6 +136,7 @@
   /* profile */
 
   def documents: Boolean = true
+  def clean: Boolean = true
 
   def threads: Int
   def jobs: Int