proper target directory for libraries;
authorwenzelm
Tue, 13 Oct 2020 19:59:28 +0200
changeset 72469 96f56191aaea
parent 72468 60471f4bafd2
child 72470 e2e9ef9aa2df
proper target directory for libraries;
src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Tue Oct 13 19:29:28 2020 +0200
+++ b/src/Pure/Admin/build_polyml.scala	Tue Oct 13 19:59:28 2020 +0200
@@ -92,9 +92,6 @@
         } || { echo "Build failed" >&2; exit 2; }
       """, redirect = true, echo = true).check
 
-    Executable.libraries_closure(
-      root + Path.explode("target/bin/poly"), mingw = mingw, filter = info.libs)
-
 
     /* sha1 library */
 
@@ -123,6 +120,9 @@
       entry <- File.read_dir(dir)
     } File.move(dir + Path.explode(entry), platform_dir)
 
+    Executable.libraries_closure(
+      platform_dir + Path.basic("poly").platform_exe, mingw = mingw, filter = info.libs)
+
 
     /* polyc: directory prefix */