| changeset 43674 | 3ddaa75c669c |
| parent 43673 | 29eb1cd29961 |
| child 44159 | 9a35e88d9dc9 |
--- a/src/Pure/Thy/thy_info.scala Tue Jul 05 22:39:15 2011 +0200 +++ b/src/Pure/Thy/thy_info.scala Tue Jul 05 22:43:18 2011 +0200 @@ -70,5 +70,5 @@ } def dependencies(dir: Path, str: String): Deps = - require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str) // FIXME capture errors in str (!??) + require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str) }