changeset 56208 | 06cc31dff138 |
parent 55825 | 694833e3e4a0 |
child 56277 | c4f75e733812 |
--- a/src/Tools/jEdit/lib/Tools/jedit Tue Mar 18 16:45:14 2014 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Tue Mar 18 17:39:03 2014 +0100 @@ -27,7 +27,7 @@ "src/jedit_editor.scala" "src/jedit_lib.scala" "src/jedit_options.scala" - "src/jedit_thy_load.scala" + "src/jedit_resources.scala" "src/monitor_dockable.scala" "src/output_dockable.scala" "src/plugin.scala"