# HG changeset patch # User wenzelm # Date 1546096385 -3600 # Node ID b8e8a724182b2c6b3126c85e9fab039d0bd774c2 # Parent 892b68f932f9fc7d81a7b113f222cec5dbd139ca unused; diff -r 892b68f932f9 -r b8e8a724182b src/Pure/Tools/dump.scala --- 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 */