backout cefeea956989: Graphview *is* required in Pure to replace old browser eventually;
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Jan 22 12:39:44 2015 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Jan 22 13:21:45 2015 +0100
@@ -53,18 +53,6 @@
"src/theories_dockable.scala"
"src/timing_dockable.scala"
"src/token_markup.scala"
- "../Graphview/graph_panel.scala"
- "../Graphview/layout.scala"
- "../Graphview/main_panel.scala"
- "../Graphview/metrics.scala"
- "../Graphview/model.scala"
- "../Graphview/mutator.scala"
- "../Graphview/mutator_dialog.scala"
- "../Graphview/mutator_event.scala"
- "../Graphview/popups.scala"
- "../Graphview/shapes.scala"
- "../Graphview/tree_panel.scala"
- "../Graphview/visualizer.scala"
)
declare -a RESOURCES=(