Admin/polyml/build
changeset 63229 f951c624c1a1
parent 62387 ad3eb2889f9a
--- a/Admin/polyml/build	Sat Jun 04 16:23:42 2016 +0200
+++ b/Admin/polyml/build	Sat Jun 04 16:54:23 2016 +0200
@@ -87,6 +87,12 @@
 )
 
 mkdir -p "$TARGET"
+for X in "$TARGET"/*
+do
+  [ -d "$X" ] && rm -rf "$X"
+done
+rm -rf "$TARGET/polyml"
+cp -a "$THIS/polyi" "$TARGET/"
 mv "$SOURCE/$TARGET/bin/"* "$TARGET/"
 mv "$SOURCE/$TARGET/lib/"* "$TARGET/"
 rmdir "$SOURCE/$TARGET/bin" "$SOURCE/$TARGET/lib"