src/Tools/jEdit/lib/Tools/jedit
changeset 56906 408b526911f7
parent 56879 ee2b61f37ad9
child 57032 cf570f3ecdc1
     1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Thu May 08 00:12:22 2014 +0200
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Thu May 08 00:14:06 2014 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4    "src/jedit_resources.scala"
     1.5    "src/monitor_dockable.scala"
     1.6    "src/output_dockable.scala"
     1.7 +  "src/pide_docking_framework.scala"
     1.8    "src/plugin.scala"
     1.9    "src/pretty_text_area.scala"
    1.10    "src/pretty_tooltip.scala"