changeset 44159 | 9a35e88d9dc9 |
parent 43674 | 3ddaa75c669c |
child 44222 | 9d5ef6cd4ee1 |
--- a/src/Pure/Thy/thy_info.scala Fri Aug 12 11:41:26 2011 +0200 +++ b/src/Pure/Thy/thy_info.scala Fri Aug 12 12:03:17 2011 +0200 @@ -38,7 +38,7 @@ /* dependencies */ - type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]] // name -> (text, header) + type Deps = Map[String, Exn.Result[(String, Thy_Header)]] // name -> (text, header) private def require_thys(ignored: String => Boolean, initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =