--- a/src/Pure/General/file.scala Fri Jan 27 15:33:21 2023 +0100
+++ b/src/Pure/General/file.scala Fri Jan 27 15:43:45 2023 +0100
@@ -404,5 +404,5 @@
/* space */
def space(path: Path): Space =
- Space.bytes(path.file.length)
+ Space.bytes(check_file(path).file.length)
}