src/Pure/Build/build_benchmark.scala
changeset 79698 b676998d7f97
parent 79682 1fa1b32b0379
child 79777 db9c6be8e236
equal deleted inserted replaced
79697:2e1f75c870e3 79698:b676998d7f97
    50 
    50 
    51         val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)
    51         val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)
    52         val session = sessions(benchmark_session)
    52         val session = sessions(benchmark_session)
    53 
    53 
    54         val hierachy = session.ancestors.map(store.output_session(_, store_heap = true))
    54         val hierachy = session.ancestors.map(store.output_session(_, store_heap = true))
    55         ML_Heap.restore(database_server, hierachy, cache = store.cache.compress)
    55         for (db <- database_server) ML_Heap.restore(db, hierachy, cache = store.cache.compress)
    56 
    56 
    57         val local_options = options + "build_database_server=false" + "build_database=false"
    57         val local_options = options + "build_database_server=false" + "build_database=false"
    58 
    58 
    59         benchmark_requirements(local_options, progress)
    59         benchmark_requirements(local_options, progress)
    60         ML_Heap.restore(database_server, hierachy, cache = store.cache.compress)
    60         for (db <- database_server) ML_Heap.restore(db, hierachy, cache = store.cache.compress)
    61 
    61 
    62         def get_shasum(session_name: String): SHA1.Shasum = {
    62         def get_shasum(session_name: String): SHA1.Shasum = {
    63           val ancestor_shasums = sessions(session_name).ancestors.map(get_shasum)
    63           val ancestor_shasums = sessions(session_name).ancestors.map(get_shasum)
    64 
    64 
    65           val input_shasum =
    65           val input_shasum =