# HG changeset patch
# User wenzelm
# Date 1344354390 -7200
# Node ID 8d381fdef89818bee2f709757da1fc5d29783a4a
# Parent  5b51ccdc8623b1a0d70a5de40057c41a475277f7
need to expand path in order to resolve imports like "~~/src/Tools/Code_Generator";

diff -r 5b51ccdc8623 -r 8d381fdef898 src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Tue Aug 07 17:08:22 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala	Tue Aug 07 17:46:30 2012 +0200
@@ -39,7 +39,7 @@
   /* file-system operations */
 
   def append(dir: String, source_path: Path): String =
-    (Path.explode(dir) + source_path).implode
+    (Path.explode(dir) + source_path).expand.implode
 
   def read_header(name: Document.Node.Name): Thy_Header =
   {