Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified output: avoid confusion with line:column notation;
  2. clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
Changeset 64546:134ae7da2ccf by wenzelm:
clarified output: avoid confusion with line:column notation;
The file was modified src/Pure/PIDE/text.scala (diff)
Changeset 64545:25045094d7bb by wenzelm:
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
The file was modified src/Pure/Admin/ci_api.scala (diff)
The file was modified src/Pure/General/json.scala (diff)