| changeset 60962 | faa452d8e265 |
| parent 60956 | 10d463883dc2 |
| child 60964 | fdb82e722f8a |
--- a/src/Pure/ML-Systems/polyml.ML Mon Aug 17 23:16:03 2015 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Mon Aug 17 23:45:12 2015 +0200 @@ -31,6 +31,8 @@ then use "ML-Systems/share_common_data_polyml-5.3.0.ML" else (); +if ML_System.platform_is_windows then use "ML-Systems/windows_polyml.ML" else (); + structure ML_System = struct