# HG changeset patch
# User wenzelm
# Date 1478862843 -3600
# Node ID 6a1a1bbfcb93fd9bc02a702c0843f22ea9042ab7
# Parent  abc34a149690e395ce8925fd0ca2e0a2d80c38af
copy libgmp on Linux;

diff -r abc34a149690 -r 6a1a1bbfcb93 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Fri Nov 11 11:41:14 2016 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Fri Nov 11 12:14:03 2016 +0100
@@ -68,6 +68,9 @@
       platform_info.get(platform) getOrElse
         error("Bad platform identifier: " + quote(platform))
 
+
+    /* configure and make */
+
     val multilib =
       platform == "x86-linux" && Isabelle_System.getenv("ISABELLE_PLATFORM64") == "x86_64-linux"
 
@@ -92,6 +95,16 @@
       progress_stdout = progress.echo(_),
       progress_stderr = progress.echo(_)).check
 
+    val lib_files =
+      if (platform.endsWith("linux")) {
+        val libs = Isabelle_System.bash("ldd target/bin/poly", cwd = root.file).check.out_lines
+        val Pattern = """\s*libgmp.*=>\s*(\S+).*""".r
+        for (Pattern(lib) <- libs) yield lib
+      }
+      else Nil
+
+
+    /* target */
 
     val target = Path.explode(platform)
     Isabelle_System.rm_tree(target)
@@ -103,7 +116,7 @@
       entry <- File.read_dir(dir)
     } File.move(dir + Path.explode(entry), target)
 
-    for (file <- "~~/Admin/polyml/polyi" :: info.copy_files)
+    for (file <- "~~/Admin/polyml/polyi" :: info.copy_files ::: lib_files)
       File.copy(Path.explode(file), target)
   }