# HG changeset patch
# User wenzelm
# Date 1683642810 -7200
# Node ID 1aa20895464ed64b82c4e00901c1d33579b8c689
# Parent  e5c146904c90e61139da6379dac42a8bf6fdbe80
tuned comments;

diff -r e5c146904c90 -r 1aa20895464e src/Pure/Concurrent/unsynchronized.ML
--- a/src/Pure/Concurrent/unsynchronized.ML	Tue May 09 16:31:08 2023 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML	Tue May 09 16:33:30 2023 +0200
@@ -49,6 +49,8 @@
 
 (* weak references *)
 
+(*see also $ML_SOURCES/basis/Weak.sml*)
+
 type 'a weak_ref = 'a ref option ref;
 
 fun weak_ref a = Weak.weak (SOME (ref a));