src/Tools/VSCode/src/vscode_main.scala
changeset 77208 a3f67a4459e1
parent 75454 295e1c9d2994
child 77483 291f5848bf55
--- a/src/Tools/VSCode/src/vscode_main.scala	Mon Feb 06 14:54:15 2023 +0100
+++ b/src/Tools/VSCode/src/vscode_main.scala	Mon Feb 06 15:04:21 2023 +0100
@@ -81,7 +81,7 @@
 
   val MANIFEST: Path = Path.explode("MANIFEST")
 
-  private def shasum_vsix(vsix_path: Path): String = {
+  private def shasum_vsix(vsix_path: Path): SHA1.Shasum = {
     val name = "extension/MANIFEST.shasum"
     def err(): Nothing = error("Cannot retrieve " + quote(name) + " from " + vsix_path)
     if (vsix_path.is_file) {
@@ -91,16 +91,16 @@
           case entry =>
             zip_file.getInputStream(entry) match {
               case null => err()
-              case stream => File.read_stream(stream)
+              case stream => SHA1.fake_shasum(File.read_stream(stream))
             }
         })
     }
     else err()
   }
 
-  private def shasum_dir(dir: Path): Option[String] = {
+  private def shasum_dir(dir: Path): Option[SHA1.Shasum] = {
     val path = dir + MANIFEST.shasum
-    if (path.is_file) Some(File.read(path)) else None
+    if (path.is_file) Some(SHA1.fake_shasum(File.read(path))) else None
   }
 
   def locate_extension(): Option[Path] = {