equal
deleted
inserted
replaced
29 |
29 |
30 if ML_System.name = "polyml-5.3.0" |
30 if ML_System.name = "polyml-5.3.0" |
31 then use "ML-Systems/share_common_data_polyml-5.3.0.ML" |
31 then use "ML-Systems/share_common_data_polyml-5.3.0.ML" |
32 else (); |
32 else (); |
33 |
33 |
|
34 fun ml_platform_path (s: string) = s; |
34 if ML_System.platform_is_windows then use "ML-Systems/windows_polyml.ML" else (); |
35 if ML_System.platform_is_windows then use "ML-Systems/windows_polyml.ML" else (); |
35 |
36 |
36 structure ML_System = |
37 structure ML_System = |
37 struct |
38 struct |
38 |
39 |