# HG changeset patch
# User wenzelm
# Date 1674830625 -3600
# Node ID 595358b9f61d25af5075b6cf816affe2ee39e471
# Parent  e3a2b3536030a123a6de60aa6a4ff7d80ac39e73
prefer strict operation: java.io.File.length returns 0 for non-existent file;

diff -r e3a2b3536030 -r 595358b9f61d src/Pure/General/file.scala
--- 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)
 }