src/Pure/Tools/ci_profile.scala
changeset 64081 38bb09ed965b
parent 64080 2e5c0bd708af
child 64115 68619fa37ca7
equal deleted inserted replaced
64080:2e5c0bd708af 64081:38bb09ed965b
    84 
    84 
    85 
    85 
    86   override final def apply(args: List[String]): Unit =
    86   override final def apply(args: List[String]): Unit =
    87   {
    87   {
    88     print_section("CONFIGURATION")
    88     print_section("CONFIGURATION")
    89     println(Build_Log.Setting.show_all())
    89     println(Build_Log.Settings.show())
    90     val props = load_properties()
    90     val props = load_properties()
    91     System.getProperties().putAll(props)
    91     System.getProperties().putAll(props)
    92 
    92 
    93     val options =
    93     val options =
    94       with_documents(Options.init())
    94       with_documents(Options.init())