# HG changeset patch
# User wenzelm
# Date 1421929305 -3600
# Node ID ca2336984f6a6b40280b974713265d9c53bc6b44
# Parent  3a0044e95ebac07a4b6de4629fbd755a12a2588a
backout cefeea956989: Graphview *is* required in Pure to replace old browser eventually;

diff -r 3a0044e95eba -r ca2336984f6a src/Tools/jEdit/lib/Tools/jedit
--- 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=(