changeset 64286 | b2f7aa1c6b75 |
parent 64285 | d7e0123a752b |
child 65056 | 002b4c8c366e |
--- a/src/Pure/Admin/ci_profile.scala Tue Oct 18 15:57:34 2016 +0200 +++ b/src/Pure/Admin/ci_profile.scala Tue Oct 18 16:48:41 2016 +0200 @@ -27,7 +27,7 @@ max_jobs = jobs, dirs = include, select_dirs = select, - system_mode = false, + system_mode = true, selection = select_sessions _) } val end_time = Time.now()