tuned;

--- a/src/Pure/Admin/build_vscodium.scala	Sat Mar 05 20:01:23 2022 +0100
+++ b/src/Pure/Admin/build_vscodium.scala	Sat Mar 05 21:14:35 2022 +0100
@@ -74,9 +74,9 @@
       dir + Path.explode(resources)
     }
 
-    def patch_resources(dir0: Path): Unit =
+    def patch_resources(base_dir: Path): Unit =
     {
-      val dir = resources_dir(dir0)
+      val dir = resources_dir(base_dir)
 
       HTML.init_fonts(dir + Path.explode("app/out/vs/base/browser/ui"))