| changeset 62468 | d97e13e5ea5b |
| parent 60982 | 67e389f67073 |
| child 62549 | 9498623b27f0 |
--- a/src/Pure/General/file.ML Mon Feb 29 15:23:13 2016 +0100 +++ b/src/Pure/General/file.ML Mon Feb 29 15:39:17 2016 +0100 @@ -45,7 +45,7 @@ (* system path representations *) val standard_path = Path.implode o Path.expand; -val platform_path = ml_platform_path o standard_path; +val platform_path = ML_System.platform_path o standard_path; val shell_quote = enclose "'" "'"; val shell_path = shell_quote o standard_path;