changeset 59290 | 569a8109eeb2 |
parent 59244 | 19b5fc4b2b38 |
child 59362 | 41f1645a4f63 |
--- a/src/Pure/build-jars Mon Jan 05 21:44:05 2015 +0100 +++ b/src/Pure/build-jars Mon Jan 05 21:47:12 2015 +0100 @@ -106,6 +106,7 @@ "../Tools/Graphview/graph_panel.scala" "../Tools/Graphview/layout.scala" "../Tools/Graphview/main_panel.scala" + "../Tools/Graphview/metrics.scala" "../Tools/Graphview/model.scala" "../Tools/Graphview/mutator_dialog.scala" "../Tools/Graphview/mutator_event.scala"