src/Pure/build-jars
changeset 67848 dd83610333de
parent 67802 32d76f08023f
child 68092 888d35a19866
     1.1 --- a/src/Pure/build-jars	Tue Mar 13 18:40:25 2018 +0100
     1.2 +++ b/src/Pure/build-jars	Tue Mar 13 19:34:42 2018 +0100
     1.3 @@ -147,6 +147,7 @@
     1.4    Tools/print_operation.scala
     1.5    Tools/profiling_report.scala
     1.6    Tools/server.scala
     1.7 +  Tools/server_commands.scala
     1.8    Tools/simplifier_trace.scala
     1.9    Tools/spell_checker.scala
    1.10    Tools/task_statistics.scala