# 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).