changeset 59441 | ab2c3597f1d3 |
parent 59392 | 02bacfc31446 |
child 59459 | 985fc55e9f27 |
--- a/src/Pure/build-jars Sun Jan 25 17:17:37 2015 +0100 +++ b/src/Pure/build-jars Sun Jan 25 17:48:14 2015 +0100 @@ -104,6 +104,7 @@ library.scala term.scala term_xml.scala + "../Tools/Graphview/graph_file.scala" "../Tools/Graphview/graph_panel.scala" "../Tools/Graphview/layout.scala" "../Tools/Graphview/main_panel.scala"