# HG changeset patch
# User wenzelm
# Date 1738697535 -3600
# Node ID 265aec8a81e4b2d9f7393219daa1ad1bc8b40e3f
# Parent  090b0ed235d210c0edb99f5620ba63fff65f1065
proper Path.print for user output (amending 9498623b27f0);

diff -r 090b0ed235d2 -r 265aec8a81e4 src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Tue Feb 04 21:50:15 2025 +0100
+++ b/src/Tools/cache_io.ML	Tue Feb 04 20:32:15 2025 +0100
@@ -70,7 +70,7 @@
     val table =
       if File.exists cache_path then
         let
-          fun err () = error ("Cache IO: corrupted cache file: " ^ File.bash_path cache_path)
+          fun err () = error ("Cache IO: corrupted cache file: " ^ Path.print cache_path)
 
           fun int_of_string s =
             (case read_int (raw_explode s) of