prefer File.full_path in accordance to check_file;
authorwenzelm
Tue, 21 Aug 2012 22:26:34 +0200
changeset 48877 51659a3819a7
parent 48876 157dd47032e0
child 48878 5e850e6fa3c3
prefer File.full_path in accordance to check_file;
src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Tue Aug 21 21:48:32 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML	Tue Aug 21 22:26:34 2012 +0200
@@ -121,7 +121,7 @@
     val path = Path.explode (Token.content_of tok);
     val files =
       command_files path (Keyword.command_files cmd)
-      |> map (Path.append dir #> (fn path => (File.read path, Path.position path)));
+      |> map (File.full_path dir #> (fn path => (File.read path, Path.position path)));
   in (dir, files) end;
 
 fun parse_files cmd =