equal
deleted
inserted
replaced
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 Build.ml_options.foreach(opt => println(opt + "=" + quote(Isabelle_System.getenv(opt)))) |
89 Build.ml_settings.foreach(a => println(a + "=" + quote(Isabelle_System.getenv(a)))) |
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()) |