# HG changeset patch
# User wenzelm
# Date 1122916848 -7200
# Node ID a69d0496a72411e5abcfb3adf3efe9bd14ee5510
# Parent  2ec0b8159e8e6bee0136c16f75c3db3849d5fb77
determine Poly/ML's idea of current hardware and operating system type;

diff -r 2ec0b8159e8e -r a69d0496a724 lib/scripts/polyml-platform
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/polyml-platform	Mon Aug 01 19:20:48 2005 +0200
@@ -0,0 +1,58 @@
+#!/usr/bin/env bash
+#
+# $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="unknown-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
+
+echo "$PLATFORM"