# HG changeset patch
# User wenzelm
# Date 1397057377 -7200
# Node ID 6437c989a744e7918edd284476db5eb8e4c590e4
# Parent  0c63f3538639d3086c5a15c65c0b18c0a8450d19
tuned comments (see Scala version);

diff -r 0c63f3538639 -r 6437c989a744 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Wed Apr 09 16:22:06 2014 +0200
+++ b/src/Pure/System/isabelle_system.ML	Wed Apr 09 17:29:37 2014 +0200
@@ -67,7 +67,7 @@
   else (system_command ("cp -p -R -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
 
 
-(* unique tmp files *)
+(* tmp files *)
 
 fun create_tmp_path name ext =
   let
@@ -80,6 +80,9 @@
   let val path = create_tmp_path name ext
   in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
 
+
+(* tmp dirs *)
+
 fun rm_tree path = system_command ("rm -r -f " ^ File.shell_path path);
 
 fun with_tmp_dir name f =