equal
deleted
inserted
replaced
1 #!/bin/sh |
1 #!/bin/sh |
|
2 # |
|
3 # $Id$ |
2 # |
4 # |
3 # polyml-platform --- determine Poly/ML's idea of current hardware and |
5 # polyml-platform --- determine Poly/ML's idea of current hardware and |
4 # operating system type |
6 # operating system type |
5 # |
7 # |
6 # NOTE: platform identifiers should be kept as generic as possible, |
8 # NOTE: platform identifiers should be kept as generic as possible, |
23 Linux) |
25 Linux) |
24 case `uname -m` in |
26 case `uname -m` in |
25 i?86) |
27 i?86) |
26 PLATFORM=x86-linux |
28 PLATFORM=x86-linux |
27 ;; |
29 ;; |
|
30 x86?64) |
|
31 PLATFORM=x86-linux |
|
32 ;; |
28 Power* | power* | ppc) |
33 Power* | power* | ppc) |
29 PLATFORM=ppc-linux |
34 PLATFORM=ppc-linux |
30 ;; |
35 ;; |
31 esac |
36 esac |
32 ;; |
37 ;; |