src/Pure/Tools/update_cartouches.scala
changeset 68994 d961e11e0e87
parent 67433 e0c0c1f0e3e7
child 69271 4cb70e7e36b9
equal deleted inserted replaced
68991:6c1beb52d766 68994:d961e11e0e87
   102       if (specs.isEmpty) getopts.usage()
   102       if (specs.isEmpty) getopts.usage()
   103 
   103 
   104       for {
   104       for {
   105         spec <- specs
   105         spec <- specs
   106         file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
   106         file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
   107       } update_cartouches(replace_text, Path.explode(File.standard_path(file)))
   107       } update_cartouches(replace_text, File.path(file))
   108     })
   108     })
   109 }
   109 }