# HG changeset patch
# User wenzelm
# Date 956143216 -7200
# Node ID 36b1657884210f56994ce41582c3e569a538aa0b
# Parent  2665170f104a1e563c31eeb1554ef9ffdd661854
check_file: keep expanded (!) absolute path;

diff -r 2665170f104a -r 36b165788421 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Apr 19 12:59:38 2000 +0200
+++ b/src/Pure/Thy/thy_load.ML	Wed Apr 19 13:20:16 2000 +0200
@@ -70,7 +70,7 @@
     val path = Path.expand src_path;
 
     fun find_ext rel_path ext =
-      let val ext_path = Path.ext ext rel_path
+      let val ext_path = Path.expand (Path.ext ext rel_path)
       in apsome (fn info => (File.full_path ext_path, info)) (File.info ext_path) end;
 
     fun find_dir dir =