author | wenzelm |
Sun, 13 Mar 2011 16:14:14 +0100 | |
changeset 41945 | 8e32c3992cb3 |
parent 41944 | b97091ae583a |
child 41946 | 380f7f5ff126 |
--- a/src/Tools/cache_io.ML Sun Mar 13 16:01:00 2011 +0100 +++ b/src/Tools/cache_io.ML Sun Mar 13 16:14:14 2011 +0100 @@ -84,7 +84,7 @@ fun make path = let val table = if File.exists path then load path else (1, Symtab.empty) - in Cache {path=path, table=Synchronized.var (Path.implode path) table} end + in Cache {path=path, table=Synchronized.var "Cache_IO" table} end fun load_cached_result cache_path (p, len1, len2) = let