# HG changeset patch # User Lars Hupel # Date 1538644215 -7200 # Node ID cbcc43a00cff300a6dab7a1692ac35eb2d9be028 # Parent 919a1b23c192300c09da05ee625768fe5b713dcc Jenkins: delete obsolete profile diff -r 919a1b23c192 -r cbcc43a00cff Admin/jenkins/build/ci_build_makeall.scala --- a/Admin/jenkins/build/ci_build_makeall.scala Wed Oct 03 20:55:59 2018 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,16 +0,0 @@ -object profile extends isabelle.CI_Profile -{ - - import isabelle._ - - def threads = 2 - def jobs = 3 - def include = Nil - def select = Nil - - def pre_hook(args: List[String]) = {} - def post_hook(results: Build.Results) = {} - - def selection = Sessions.Selection(all_sessions = true) - -}