changeset 71726 | a5fda30edae2 |
parent 71624 | f0499449e149 |
child 71939 | 107472ccc60d |
--- a/src/Pure/Thy/export.scala Tue Apr 07 21:07:28 2020 +0200 +++ b/src/Pure/Thy/export.scala Tue Apr 07 21:49:36 2020 +0200 @@ -299,7 +299,7 @@ store: Sessions.Store, session_name: String, export_dir: Path, - progress: Progress = No_Progress, + progress: Progress = new Progress, export_prune: Int = 0, export_list: Boolean = false, export_patterns: List[String] = Nil)