# HG changeset patch
# User wenzelm
# Date 1545924739 -3600
# Node ID 0428fd0a13b7c750c608771458dbe435717038cb
# Parent  16779868de1fe131ede528b8d7a0ea338baf1275
tuned;

diff -r 16779868de1f -r 0428fd0a13b7 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Thu Dec 27 16:56:53 2018 +0100
+++ b/src/Pure/Tools/dump.scala	Thu Dec 27 16:32:19 2018 +0100
@@ -39,7 +39,7 @@
     override def toString: String = name
   }
 
-  val known_aspects =
+  val known_aspects: List[Aspect] =
     List(
       Aspect("markup", "PIDE markup (YXML format)",
         { case args =>