# HG changeset patch # User Lars Hupel # Date 1476799054 -7200 # Node ID d7e0123a752b5c95a395e0e248361e0b16a1e6d2 # Parent f3b905b2eee23cf28da3892204f444f378b071a7 Jenkins: configurable clean build diff -r f3b905b2eee2 -r d7e0123a752b src/Pure/Admin/ci_profile.scala --- a/src/Pure/Admin/ci_profile.scala Tue Oct 18 12:01:54 2016 +0200 +++ b/src/Pure/Admin/ci_profile.scala Tue Oct 18 15:57:34 2016 +0200 @@ -22,7 +22,7 @@ Build.build_selection( options = options, progress = progress, - clean_build = true, + clean_build = clean, verbose = true, max_jobs = jobs, dirs = include, @@ -136,6 +136,7 @@ /* profile */ def documents: Boolean = true + def clean: Boolean = true def threads: Int def jobs: Int