tuned comment (cf. e9f26e66692d);
authorwenzelm
Tue, 05 Jul 2011 22:43:18 +0200
changeset 43674 3ddaa75c669c
parent 43673 29eb1cd29961
child 43675 8252d51d70e2
tuned comment (cf. e9f26e66692d);
src/Pure/Thy/thy_info.scala
--- 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)
 }