| changeset 76509 | b01b0014c3f9 |
| parent 76507 | 78a2030240f1 |
| child 77570 | 98b4a9902582 |
--- a/src/Pure/General/js.scala Fri Nov 11 23:04:55 2022 +0100 +++ b/src/Pure/General/js.scala Fri Nov 11 23:25:24 2022 +0100 @@ -35,5 +35,5 @@ string(File.standard_path(p) + (if (dir) "/" else "")) def platform_path(p: Path, dir: Boolean = false): Source = - string(File.platform_path(p) + (if (dir) File.platform_path(Path.root) else "")) + string(File.platform_path(p) + (if (dir) "/" else "")) }