--- a/src/Pure/Admin/build_csdp.scala Sun Oct 11 12:14:58 2020 +0200
+++ b/src/Pure/Admin/build_csdp.scala Sun Oct 11 12:48:48 2020 +0200
@@ -20,9 +20,11 @@
val changed: List[(String, String)] =
List("CFLAGS" -> CFLAGS, "LIBS" -> LIBS).filter(p => p._2.nonEmpty)
- def print: String =
- if (changed.isEmpty) ""
- else " * " + platform + ":\n" + changed.map(p => " " + p._1 + "=" + p._2).mkString("\n")
+ def print: Option[String] =
+ if (changed.isEmpty) None
+ else
+ Some(" * " + platform + ":\n" + changed.map(p => " " + p._1 + "=" + p._2)
+ .mkString("\n"))
def change(path: Path)
{
@@ -163,7 +165,8 @@
Makefile flags have been changed for various platforms as follows:
-""" + build_flags.map(_.print).mkString("\n\n") + """
+""" + build_flags.flatMap(_.print).mkString("\n\n") + """
+
The distribution has been built like this:
cd src && make