tuned;
authorwenzelm
Tue Dec 20 08:46:38 2016 +0100 (2016-12-20)
changeset 646097cc4b49be1ea
parent 64606 a871fa7c24fc
child 64610 1b89608974e9
tuned;
src/Pure/build-jars
     1.1 --- a/src/Pure/build-jars	Mon Dec 19 20:46:15 2016 +0100
     1.2 +++ b/src/Pure/build-jars	Tue Dec 20 08:46:38 2016 +0100
     1.3 @@ -141,25 +141,25 @@
     1.4    library.scala
     1.5    term.scala
     1.6    term_xml.scala
     1.7 -  "../Tools/Graphview/graph_file.scala"
     1.8 -  "../Tools/Graphview/graph_panel.scala"
     1.9 -  "../Tools/Graphview/graphview.scala"
    1.10 -  "../Tools/Graphview/layout.scala"
    1.11 -  "../Tools/Graphview/main_panel.scala"
    1.12 -  "../Tools/Graphview/metrics.scala"
    1.13 -  "../Tools/Graphview/model.scala"
    1.14 -  "../Tools/Graphview/mutator.scala"
    1.15 -  "../Tools/Graphview/mutator_dialog.scala"
    1.16 -  "../Tools/Graphview/mutator_event.scala"
    1.17 -  "../Tools/Graphview/popups.scala"
    1.18 -  "../Tools/Graphview/shapes.scala"
    1.19 -  "../Tools/Graphview/tree_panel.scala"
    1.20 -  "../Tools/VSCode/src/channel.scala"
    1.21 -  "../Tools/VSCode/src/document_model.scala"
    1.22 -  "../Tools/VSCode/src/line.scala"
    1.23 -  "../Tools/VSCode/src/protocol.scala"
    1.24 -  "../Tools/VSCode/src/server.scala"
    1.25 -  "../Tools/VSCode/src/uri_resources.scala"
    1.26 +  ../Tools/Graphview/graph_file.scala
    1.27 +  ../Tools/Graphview/graph_panel.scala
    1.28 +  ../Tools/Graphview/graphview.scala
    1.29 +  ../Tools/Graphview/layout.scala
    1.30 +  ../Tools/Graphview/main_panel.scala
    1.31 +  ../Tools/Graphview/metrics.scala
    1.32 +  ../Tools/Graphview/model.scala
    1.33 +  ../Tools/Graphview/mutator.scala
    1.34 +  ../Tools/Graphview/mutator_dialog.scala
    1.35 +  ../Tools/Graphview/mutator_event.scala
    1.36 +  ../Tools/Graphview/popups.scala
    1.37 +  ../Tools/Graphview/shapes.scala
    1.38 +  ../Tools/Graphview/tree_panel.scala
    1.39 +  ../Tools/VSCode/src/channel.scala
    1.40 +  ../Tools/VSCode/src/document_model.scala
    1.41 +  ../Tools/VSCode/src/line.scala
    1.42 +  ../Tools/VSCode/src/protocol.scala
    1.43 +  ../Tools/VSCode/src/server.scala
    1.44 +  ../Tools/VSCode/src/uri_resources.scala
    1.45  )
    1.46  
    1.47