tuned;
authorwenzelm
Thu, 02 Dec 2010 10:44:33 +0100
changeset 40851 58d25beedcea
parent 40850 d804de9ac970
child 40852 aee98c88c587
tuned;
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