allow spaces in SCALA_HOME directory name;
authorwenzelm
Mon, 17 Oct 2022 20:24:15 +0200
changeset 76327 f70b015e4ac1
parent 76326 a39fa81929d4
child 76328 79ef5d0fff00
allow spaces in SCALA_HOME directory name;
Admin/components/components.sha1
Admin/components/main
src/Pure/Admin/build_scala.scala
--- a/Admin/components/components.sha1	Mon Oct 17 20:18:05 2022 +0200
+++ b/Admin/components/components.sha1	Mon Oct 17 20:24:15 2022 +0200
@@ -425,6 +425,7 @@
 b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz
 5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz
 97c5b73011f4d6438b616e5940e6d759034f5414 scala-3.1.3.tar.gz
+87c8e53100df4bc85cd8d4f55028088646d70fb4 scala-3.2.0-1.tar.gz
 7677b02fe06c992ca6cf82bf68adb16287294256 scala-3.2.0.tar.gz
 abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz
 cbd491c0feba1d21019d05564e76dd04f592ccb4 spass-3.8ds-1.tar.gz
--- a/Admin/components/main	Mon Oct 17 20:18:05 2022 +0200
+++ b/Admin/components/main	Mon Oct 17 20:24:15 2022 +0200
@@ -22,7 +22,7 @@
 pdfjs-2.14.305
 polyml-test-bafe319bc3a6-1
 postgresql-42.5.0
-scala-3.2.0
+scala-3.2.0-1
 smbc-0.4.1
 spass-3.8ds-2
 sqlite-jdbc-3.36.0.3
--- a/src/Pure/Admin/build_scala.scala	Mon Oct 17 20:18:05 2022 +0200
+++ b/src/Pure/Admin/build_scala.scala	Mon Oct 17 20:24:15 2022 +0200
@@ -123,12 +123,25 @@
 """ + terminate_lines(classpath.map(jar => "classpath \"$SCALA_HOME/lib/" + jar + "\"")))
 
 
+    /* adhoc changes */
+
+    val patched_scripts = List("bin/scala", "bin/scalac")
+    for (name <- patched_scripts) {
+      File.change(component_dir + Path.explode(name)) {
+        _.replace(""""-Dscala.home=$PROG_HOME"""", """"-Dscala.home=\"$PROG_HOME\""""")
+      }
+    }
+
+
     /* README */
 
     File.write(component_dir + Path.basic("README"),
       "This distribution of Scala integrates the following parts:\n\n" +
       (main_download :: lib_downloads).map(_.print).mkString("\n\n") + """
 
+Minor changes to """ + patched_scripts.mkString(" and ") + """ allow an installation location
+with spaces in the directory name.
+
 
         Makarius
         """ + Date.Format.date(Date.now()) + "\n")