equal
deleted
inserted
replaced
297 |
297 |
298 def export_files( |
298 def export_files( |
299 store: Sessions.Store, |
299 store: Sessions.Store, |
300 session_name: String, |
300 session_name: String, |
301 export_dir: Path, |
301 export_dir: Path, |
302 progress: Progress = No_Progress, |
302 progress: Progress = new Progress, |
303 export_prune: Int = 0, |
303 export_prune: Int = 0, |
304 export_list: Boolean = false, |
304 export_list: Boolean = false, |
305 export_patterns: List[String] = Nil) |
305 export_patterns: List[String] = Nil) |
306 { |
306 { |
307 using(store.open_database(session_name))(db => |
307 using(store.open_database(session_name))(db => |