equal
deleted
inserted
replaced
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 } |