equal
deleted
inserted
replaced
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 object Build_PolyML |
10 object Build_PolyML |
11 { |
11 { |
|
12 /** build_polyml **/ |
|
13 |
12 sealed case class Platform_Info( |
14 sealed case class Platform_Info( |
13 options: List[String] = Nil, |
15 options: List[String] = Nil, |
14 options_multilib: List[String] = Nil, |
16 options_multilib: List[String] = Nil, |
15 setup: String = "", |
17 setup: String = "", |
16 copy_files: List[String] = Nil) |
18 copy_files: List[String] = Nil) |
141 for (file <- "~~/Admin/polyml/polyi" :: info.copy_files ::: ldd_files ::: sha1_files) |
143 for (file <- "~~/Admin/polyml/polyi" :: info.copy_files ::: ldd_files ::: sha1_files) |
142 File.copy(Path.explode(file), target) |
144 File.copy(Path.explode(file), target) |
143 } |
145 } |
144 |
146 |
145 |
147 |
|
148 |
146 /** command line entry point **/ |
149 /** command line entry point **/ |
147 |
150 |
148 def main(args: Array[String]) |
151 def main(args: Array[String]) |
149 { |
152 { |
150 Command_Line.tool0 { |
153 Command_Line.tool0 { |