tuned header;
authorwenzelm
Wed Jun 06 14:18:31 2018 +0200 (11 months ago)
changeset 683967433ee1ed7e3
parent 68395 76a0f3bafb16
child 68397 cace81744c61
tuned header;
src/Pure/General/cache.scala
     1.1 --- a/src/Pure/General/cache.scala	Wed Jun 06 14:18:25 2018 +0200
     1.2 +++ b/src/Pure/General/cache.scala	Wed Jun 06 14:18:31 2018 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -/*  Title:      Pure/cache.scala
     1.5 +/*  Title:      Pure/General/cache.scala
     1.6      Author:     Makarius
     1.7  
     1.8  cache for partial sharing (weak table).