# HG changeset patch
# User wenzelm
# Date 1188293131 -7200
# Node ID bb7a85ea57cf49ad5deaa87cb12c84f1ead120e4
# Parent  cad0644294a9250a385cc83c3bf729543f7b69d3
norm_absolute: CRITICAL;

diff -r cad0644294a9 -r bb7a85ea57cf src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Tue Aug 28 11:25:30 2007 +0200
+++ b/src/Pure/General/file.ML	Tue Aug 28 11:25:31 2007 +0200
@@ -56,13 +56,13 @@
 val cd = cd o platform_path;
 val pwd = explode_platform_path o pwd;
 
-fun norm_absolute p =
+fun norm_absolute p = NAMED_CRITICAL "IO" (fn () =>
   let
     val p' = pwd ();
     fun norm p = if can cd p then pwd ()
       else Path.append (norm (Path.dir p)) (Path.base p);
     val p'' = norm p;
-  in (cd p'; p'') end
+  in (cd p'; p'') end);
 
 fun full_path path =
   (if Path.is_absolute path then path