--- a/src/Tools/jEdit/src/readme_dockable.scala Mon Sep 24 21:16:33 2012 +0200
+++ b/src/Tools/jEdit/src/readme_dockable.scala Tue Sep 25 12:17:58 2012 +0200
@@ -12,7 +12,7 @@
import org.gjt.sp.jedit.View
-class README_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
+class README_Dockable(view: View, position: String) extends Dockable(view, position)
{
private val readme = new HTML_Panel("SansSerif", 14)
private val readme_path = Path.explode("$JEDIT_HOME/README.html")