Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned;
  2. more documentation;
  3. retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;
  4. clarified platform file operations;
  5. more operations;
  6. clarified signature;
  7. more robust: always package;
  8. prefer explicit link;
Changeset 66237:93eac3bdf3f9 by wenzelm:
tuned;
The file was modified src/Tools/VSCode/extension/README.md (diff)
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 66236:8ae7c5ba1a85 by wenzelm:
more documentation;
The file was modified src/Tools/VSCode/extension/README.md (diff)
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 66235:d4fa51e7c4ff by wenzelm:
retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;
The file was modified src/Pure/General/url.scala (diff)
The file was modified src/Tools/VSCode/src/protocol.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_rendering.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
Changeset 66234:836898197296 by wenzelm:
clarified platform file operations;
The file was modified src/Pure/General/url.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/imports.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_rendering.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
The file was modified src/Tools/jEdit/src/scala_console.scala (diff)
Changeset 66233:7188967253e5 by wenzelm:
more operations;
The file was modified src/Pure/General/file.scala (diff)
Changeset 66232:be0ab4b94c62 by wenzelm:
clarified signature;
The file was modified src/Pure/General/file.scala (diff)
The file was modified src/Pure/General/path.scala (diff)
Changeset 66231:406b5ae7f5f3 by wenzelm:
more robust: always package;
The file was modified src/Tools/VSCode/src/build_vscode.scala (diff)
Changeset 66230:ae814012b95f by wenzelm:
prefer explicit link;
The file was modified src/Tools/VSCode/extension/README.md (diff)
The file was modified src/Tools/VSCode/extension/package.json (diff)
The file was modified src/Tools/VSCode/src/build_vscode.scala (diff)