# HG changeset patch
# User wenzelm
# Date 1291402977 -3600
# Node ID d5729fd13ca8daf244f8eb4f38118e729e772312
# Parent  e08fa125c268cb4626ed6bb7cfd90f3cb59c90ff
comment;

diff -r e08fa125c268 -r d5729fd13ca8 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Fri Dec 03 18:29:49 2010 +0100
+++ b/src/Pure/Thy/present.ML	Fri Dec 03 20:02:57 2010 +0100
@@ -489,7 +489,7 @@
 
 
 
-(** draft document output **)
+(** draft document output **)  (* FIXME doc_path etc. not thread-safe *)
 
 fun drafts doc_format src_paths =
   let