# HG changeset patch
# User wenzelm
# Date 1413449983 -7200
# Node ID 4c9aa5f7bfa0fadd2ce104c38069119d2a08d391
# Parent  80832ae207adde6d7c3363962b8991d854b04b3b
proper type comparison (amending cd4439d8799c);

diff -r 80832ae207ad -r 4c9aa5f7bfa0 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Thu Oct 16 10:43:34 2014 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Thu Oct 16 10:59:43 2014 +0200
@@ -181,7 +181,7 @@
     override def hashCode: Int = context.hashCode
     override def equals(that: Any): Boolean =
       that match {
-        case other: Line_Context => context == other.context
+        case other: Generic_Line_Context[_] => context == other.context
         case _ => false
       }
   }