# HG changeset patch
# User wenzelm
# Date 1291283073 -3600
# Node ID 58d25beedcea2900d82af0905b86edd8e6711d97
# Parent  d804de9ac97055432580a07b2a3e1058e59ccae8
tuned;

diff -r d804de9ac970 -r 58d25beedcea src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Wed Dec 01 21:23:21 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Thu Dec 02 10:44:33 2010 +0100
@@ -63,7 +63,7 @@
       extends TokenMarker.LineContext(dummy_rules, prev)
     {
       override def hashCode: Int = line
-      override def equals(that: Any) =
+      override def equals(that: Any): Boolean =
         that match {
           case other: Line_Context => line == other.line
           case _ => false