src/Pure/build-jars
changeset 72767 f6bf65554764
parent 72761 4519eeefe3b5
child 72886 ac64b753a65f
--- a/src/Pure/build-jars	Sat Nov 28 23:30:25 2020 +0100
+++ b/src/Pure/build-jars	Sat Nov 28 23:36:17 2020 +0100
@@ -205,11 +205,11 @@
   src/Tools/VSCode/src/build_vscode.scala
   src/Tools/VSCode/src/channel.scala
   src/Tools/VSCode/src/dynamic_output.scala
-  src/Tools/VSCode/src/grammar.scala
   src/Tools/VSCode/src/language_server.scala
   src/Tools/VSCode/src/lsp.scala
   src/Tools/VSCode/src/preview_panel.scala
   src/Tools/VSCode/src/state_panel.scala
+  src/Tools/VSCode/src/textmate_grammar.scala
   src/Tools/VSCode/src/vscode_model.scala
   src/Tools/VSCode/src/vscode_rendering.scala
   src/Tools/VSCode/src/vscode_resources.scala