equal
deleted
inserted
replaced
87 compile(dir + Path.basic(name + ".scala")) |
87 compile(dir + Path.basic(name + ".scala")) |
88 case dir if is_external(dir, name) => |
88 case dir if is_external(dir, name) => |
89 (args: List[String]) => |
89 (args: List[String]) => |
90 { |
90 { |
91 val tool = dir + Path.basic(name) |
91 val tool = dir + Path.basic(name) |
92 val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args)) |
92 val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args)) |
93 sys.exit(result.print_stdout.rc) |
93 sys.exit(result.print_stdout.rc) |
94 } |
94 } |
95 }) |
95 }) |
96 |
96 |
97 |
97 |