equal
deleted
inserted
replaced
92 progress_stderr = progress.echo_if(verbose, _)).check |
92 progress_stderr = progress.echo_if(verbose, _)).check |
93 |
93 |
94 |
94 |
95 /* install */ |
95 /* install */ |
96 |
96 |
97 File.copy(build_dir + Path.basic("LICENCE"), component_dir + Path.basic("LICENSE")) |
97 Isabelle_System.copy_file(build_dir + Path.basic("LICENCE"), |
|
98 component_dir + Path.basic("LICENSE")) |
98 |
99 |
99 val install_files = List("SPASS") |
100 val install_files = List("SPASS") |
100 for (name <- install_files ::: install_files.map(_ + ".exe")) { |
101 for (name <- install_files ::: install_files.map(_ + ".exe")) { |
101 val path = build_dir + Path.basic(name) |
102 val path = build_dir + Path.basic(name) |
102 if (path.is_file) File.copy(path, platform_dir) |
103 if (path.is_file) Isabelle_System.copy_file(path, platform_dir) |
103 } |
104 } |
104 |
105 |
105 |
106 |
106 /* settings */ |
107 /* settings */ |
107 |
108 |