changeset 76831 | 72daee8a39ca |
parent 76348 | a15f16e8ad18 |
child 76884 | a004c5322ea4 |
--- a/src/Pure/General/path.scala Fri Dec 30 21:09:50 2022 +0100 +++ b/src/Pure/General/path.scala Fri Dec 30 21:27:57 2022 +0100 @@ -312,8 +312,6 @@ } catch { case ERROR(_) => None }).headOption.getOrElse(implode) } - def position: Position.T = Position.File(implode_symbolic) - /* platform files */