# HG changeset patch
# User wenzelm
# Date 1309898598 -7200
# Node ID 3ddaa75c669ce5891b0157e919a4a595dc05a9f4
# Parent  29eb1cd299614bbded989f04942744b0e9bf4e6d
tuned comment (cf. e9f26e66692d);

diff -r 29eb1cd29961 -r 3ddaa75c669c 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)
 }