# HG changeset patch
# User wenzelm
# Date 1122916848 -7200
# Node ID 5b344d1dccd85964c6dae4dff215533225cda417
# Parent  a69d0496a72411e5abcfb3adf3efe9bd14ee5510
obsolete;

diff -r a69d0496a724 -r 5b344d1dccd8 Admin/polyml/bin/polyml
--- a/Admin/polyml/bin/polyml	Mon Aug 01 19:20:48 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-#!/bin/sh
-#
-# platform independent Poly/ML wrapper script
-
-
-## self references
-
-PRG="`basename "$0"`"
-
-if [ -h "$0" ]; then
-  THIS="`cd "\`dirname "$0"\`"; cd "\`dirname "\\\`ls -l "$PRG" | sed -e 's/^.* -> //'\\\`"\`"; pwd`"
-else
-  THIS="`cd "\`dirname "$0"\`"; pwd`"
-fi
-
-SUPER="`cd "$THIS/.."; pwd`"
-
-
-## run poly
-
-PLATFORM=`"$THIS/polyml-platform"`
-exec "$SUPER/$PLATFORM/poly" $*
diff -r a69d0496a724 -r 5b344d1dccd8 Admin/polyml/bin/polyml-platform
--- a/Admin/polyml/bin/polyml-platform	Mon Aug 01 19:20:48 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-#!/bin/sh
-#
-# $Id$
-#
-# polyml-platform --- determine Poly/ML's idea of current hardware and
-# operating system type
-#
-# NOTE: platform identifiers should be kept as generic as possible,
-# i.e. shared by compatible environments.
-
-PLATFORM=""
-
-case `uname -s` in
-  SunOS)
-    case `uname -r` in
-      5.*)
-        case `uname -p` in
-          sparc)
-            PLATFORM=sparc-solaris
-            ;;
-        esac
-        ;;
-    esac
-    ;;
-  Linux)
-    case `uname -m` in
-      i?86 | x86_64)
-        PLATFORM=x86-linux
-        ;;
-      Power* | power* | ppc)
-        PLATFORM=ppc-linux
-        ;;
-    esac
-    ;;
-  FreeBSD|NetBSD)
-    case `uname -m` in
-      i?86)
-        PLATFORM=x86-bsd
-        ;;
-    esac
-    ;;
-  Darwin)
-    case `uname -m` in
-      Power* | power* | ppc)
-        PLATFORM=ppc-darwin
-        ;;
-    esac
-    ;;
-  Windows_NT)
-    case `uname -m` in
-      ?86)
-        PLATFORM=x86-win32
-        ;;
-    esac
-    ;;
-esac
-
-
-if [ -z "$PLATFORM" ]; then
-  echo "Unknown Poly/ML platform" >&2
-  exit 1
-else
-  echo "$PLATFORM"
-fi
diff -r a69d0496a724 -r 5b344d1dccd8 Admin/polyml/bin/polyml-version
--- a/Admin/polyml/bin/polyml-version	Mon Aug 01 19:20:48 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-#!/bin/sh
-#
-# $Id$
-#
-# polyml-version --- issue Poly/ML version identifier
-#
-# NOTE: version identifiers should be kept as generic as possible,
-# i.e. shared by compatible environments.
-
-echo polyml-4.1.3