equal
deleted
inserted
replaced
42 |
42 |
43 override final def apply(args: List[String]): Unit = |
43 override final def apply(args: List[String]): Unit = |
44 { |
44 { |
45 List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS").foreach(print_variable) |
45 List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS").foreach(print_variable) |
46 val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME")) |
46 val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME")) |
47 println(s"Build for repository Isabelle/${hg_id(isabelle_home)}") |
47 println(s"Build for Isabelle id ${hg_id(isabelle_home)}") |
48 |
48 |
49 val options = |
49 val options = |
50 Options.init() |
50 Options.init() |
51 .bool.update("browser_info", true) |
51 .bool.update("browser_info", true) |
52 .string.update("document", "pdf") |
52 .string.update("document", "pdf") |