Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper join without delimiter;
  2. more accurate token types; keep untyped tokens for complete covering;
  3. clarified JS namespace;
Changeset 76512:c3b4e5e4c4e5 by wenzelm:
proper join without delimiter;
The file was modified src/Pure/Tools/prismjs.scala (diff)
Changeset 76511:ec8c04dac257 by wenzelm:
more accurate token types;<br>keep untyped tokens for complete covering;
The file was modified src/Pure/Tools/prismjs.scala (diff)
Changeset 76510:b0ad975cd25b by wenzelm:
clarified JS namespace;
The file was modified src/Pure/System/nodejs.scala (diff)
The file was modified src/Pure/Tools/prismjs.scala (diff)