# HG changeset patch # User wenzelm # Date 1528287511 -7200 # Node ID 7433ee1ed7e39bef13dfe0127f65ed354da35b7f # Parent 76a0f3bafb16a138e3c48beb67783f3e9ff2d0e6 tuned header; diff -r 76a0f3bafb16 -r 7433ee1ed7e3 src/Pure/General/cache.scala --- a/src/Pure/General/cache.scala Wed Jun 06 14:18:25 2018 +0200 +++ b/src/Pure/General/cache.scala Wed Jun 06 14:18:31 2018 +0200 @@ -1,4 +1,4 @@ -/* Title: Pure/cache.scala +/* Title: Pure/General/cache.scala Author: Makarius cache for partial sharing (weak table).