src/Tools/jEdit/src/fold_handling.scala

--- a/src/Tools/jEdit/src/fold_handling.scala	Wed Aug 07 17:23:40 2013 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala	Wed Aug 07 19:59:58 2013 +0200
@@ -31,7 +31,7 @@
         if (i < 0) 0
         else {
           rendering.fold_depth(Text.Range(i, i + 1)).map(_.info) match {
-            case d #:: _ => d
+            case d :: _ => d
             case _ => 0
           }
         }