src/Pure/System/build.scala
changeset 49696 3003c87f7814
parent 49131 aa1e2ba3c697
child 49951 119440fe1d5c
equal deleted inserted replaced
49695:8f61d1c7dded 49696:3003c87f7814
   372 
   372 
   373           if (list_files)
   373           if (list_files)
   374             echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
   374             echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
   375 
   375 
   376           val sources =
   376           val sources =
   377             try { all_files.map(p => (p, SHA1.digest(p))) }
   377             try { all_files.map(p => (p, SHA1.digest(p.file))) }
   378             catch {
   378             catch {
   379               case ERROR(msg) =>
   379               case ERROR(msg) =>
   380                 error(msg + "\nThe error(s) above occurred in session " +
   380                 error(msg + "\nThe error(s) above occurred in session " +
   381                   quote(name) + Position.here(info.pos))
   381                   quote(name) + Position.here(info.pos))
   382             }
   382             }