# HG changeset patch
# User wenzelm
# Date 1465052063 -7200
# Node ID f951c624c1a1430ee0cd7778daa01b02d94395f2
# Parent  acfa595636c77d6c85e1158b27db500eb3938012
updated to recent changes of Poly/ML directory layout;

diff -r acfa595636c7 -r f951c624c1a1 Admin/polyml/CHECKLIST
--- a/Admin/polyml/CHECKLIST	Sat Jun 04 16:23:42 2016 +0200
+++ b/Admin/polyml/CHECKLIST	Sat Jun 04 16:54:23 2016 +0200
@@ -12,5 +12,3 @@
 * include sha1 source and binary for each platform
 
 * linux: include copy of libgmp.so with symlinks from build host
-
-* include copy of "polyml" script
diff -r acfa595636c7 -r f951c624c1a1 Admin/polyml/build
--- 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"
diff -r acfa595636c7 -r f951c624c1a1 Admin/polyml/polyi
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/polyml/polyi	Sat Jun 04 16:54:23 2016 +0200
@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+#
+# Portable Poly/ML command-line tool
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+
+export LD_LIBRARY_PATH="$THIS:$LD_LIBRARY_PATH"
+export DYLD_LIBRARY_PATH="$THIS:$DYLD_LIBRARY_PATH"
+
+if type -p rlwrap > /dev/null
+then
+  exec rlwrap "$THIS/poly" "$@"
+else
+  exec "$THIS/poly" "$@"
+fi
diff -r acfa595636c7 -r f951c624c1a1 Admin/polyml/polyml
--- a/Admin/polyml/polyml	Sat Jun 04 16:23:42 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-#
-# Minimal Poly/ML startup script
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-
-export LD_LIBRARY_PATH="$THIS:$LD_LIBRARY_PATH"
-export DYLD_LIBRARY_PATH="$THIS:$DYLD_LIBRARY_PATH"
-
-exec "$THIS/poly" "$@"