# HG changeset patch
# User wenzelm
# Date 1646511275 -3600
# Node ID 5e87e4fb68d2edd054a3bb825aafd7721c47330a
# Parent  05f677e641784a36caa0ee39330f8716517dbcdf
tuned;

diff -r 05f677e64178 -r 5e87e4fb68d2 src/Pure/Admin/build_vscodium.scala
--- 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"))