author | wenzelm |
Sat, 29 Dec 2018 16:13:05 +0100 | |
changeset 69537 | b8e8a724182b |
parent 69536 | 892b68f932f9 |
child 69538 | faf547d2834c |
--- a/src/Pure/Tools/dump.scala Sat Dec 29 16:11:24 2018 +0100 +++ b/src/Pure/Tools/dump.scala Sat Dec 29 16:13:05 2018 +0100 @@ -81,7 +81,6 @@ log: Logger = No_Logger, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, - system_mode: Boolean = false, selection: Sessions.Selection = Sessions.Selection.empty) { /* dependencies */