# HG changeset patch
# User haftmann
# Date 1421862002 -3600
# Node ID cefeea95698935dd053ee592038605303fc9d2ae
# Parent  ef1edfb36af7e9799b5eca600bdc39b2e3f79dc7
sufficent to have graphview as part of jEdit rather than Pure

diff -r ef1edfb36af7 -r cefeea956989 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Wed Jan 21 18:40:00 2015 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Jan 21 18:40:02 2015 +0100
@@ -53,6 +53,18 @@
   "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=(