# HG changeset patch
# User wenzelm
# Date 1536401895 -7200
# Node ID ce68b14886129cf9ae454605abe2a62fece8fce0
# Parent  e564605d4cacca00c23561a4aaa5e8fa1ed752cf
tuned signature;

diff -r e564605d4cac -r ce68b1488612 src/Pure/General/value.scala
--- a/src/Pure/General/value.scala	Sat Sep 08 12:01:37 2018 +0200
+++ b/src/Pure/General/value.scala	Sat Sep 08 12:18:15 2018 +0200
@@ -51,4 +51,12 @@
     def parse(s: java.lang.String): scala.Double =
       unapply(s) getOrElse error("Bad real: " + quote(s))
   }
+
+  object Seconds
+  {
+    def apply(x: Time): java.lang.String = x.toString
+    def unapply(s: java.lang.String): Option[Time] = Double.unapply(s).map(Time.seconds(_))
+    def parse(s: java.lang.String): Time =
+      unapply(s) getOrElse error("Bad real (for seconds): " + quote(s))
+  }
 }
diff -r e564605d4cac -r ce68b1488612 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sat Sep 08 12:01:37 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Sat Sep 08 12:18:15 2018 +0200
@@ -221,7 +221,7 @@
 """ + Library.prefix_lines("    ", show_aspects) + "\n",
       "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
-      "C:" -> (arg => commit_clean_delay = Time.seconds(Value.Double.parse(arg))),
+      "C:" -> (arg => commit_clean_delay = Value.Seconds.parse(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "O:" -> (arg => output_dir = Path.explode(arg)),
       "R" -> (_ => requirements = true),