equal
deleted
inserted
replaced
194 def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text) |
194 def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text) |
195 |
195 |
196 def write_backup(path: Path, text: CharSequence) |
196 def write_backup(path: Path, text: CharSequence) |
197 { |
197 { |
198 path.file renameTo path.backup.file |
198 path.file renameTo path.backup.file |
199 File.write(path, text) |
199 write(path, text) |
200 } |
200 } |
201 |
201 |
202 def write_backup2(path: Path, text: CharSequence) |
202 def write_backup2(path: Path, text: CharSequence) |
203 { |
203 { |
204 path.file renameTo path.backup2.file |
204 path.file renameTo path.backup2.file |
205 File.write(path, text) |
205 write(path, text) |
206 } |
206 } |
207 |
207 |
208 |
208 |
209 /* copy */ |
209 /* copy */ |
210 |
210 |