src/Tools/jEdit/lib/Tools/jedit
changeset 59424 ca2336984f6a
parent 59421 cefeea956989
child 59571 1081f91c0662
equal deleted inserted replaced
59423:3a0044e95eba 59424:ca2336984f6a
    51   "src/syslog_dockable.scala"
    51   "src/syslog_dockable.scala"
    52   "src/text_overview.scala"
    52   "src/text_overview.scala"
    53   "src/theories_dockable.scala"
    53   "src/theories_dockable.scala"
    54   "src/timing_dockable.scala"
    54   "src/timing_dockable.scala"
    55   "src/token_markup.scala"
    55   "src/token_markup.scala"
    56   "../Graphview/graph_panel.scala"
       
    57   "../Graphview/layout.scala"
       
    58   "../Graphview/main_panel.scala"
       
    59   "../Graphview/metrics.scala"
       
    60   "../Graphview/model.scala"
       
    61   "../Graphview/mutator.scala"
       
    62   "../Graphview/mutator_dialog.scala"
       
    63   "../Graphview/mutator_event.scala"
       
    64   "../Graphview/popups.scala"
       
    65   "../Graphview/shapes.scala"
       
    66   "../Graphview/tree_panel.scala"
       
    67   "../Graphview/visualizer.scala"
       
    68 )
    56 )
    69 
    57 
    70 declare -a RESOURCES=(
    58 declare -a RESOURCES=(
    71   "src/actions.xml"
    59   "src/actions.xml"
    72   "src/dockables.xml"
    60   "src/dockables.xml"