author | wenzelm |
Mon, 14 Oct 2019 20:29:19 +0200 | |
changeset 70866 | 209327bd3e3e |
parent 70865 | 4739030a5bf2 |
child 70867 | 4c8e28dabbc4 |
--- a/src/Pure/Tools/dump.scala Mon Oct 14 20:22:37 2019 +0200 +++ b/src/Pure/Tools/dump.scala Mon Oct 14 20:29:19 2019 +0200 @@ -182,7 +182,8 @@ /* resources */ def options: Options = context.session_options - def progress: Progress = context.progress + + private def progress: Progress = context.progress private val selected_session = selected_sessions.toSet