| changeset 29145 | b1c6f4563df7 |
| parent 25348 | 510b46987886 |
| child 36201 | 07d4f74abd12 |
| 29144:ca186ebbd824 | 29145:b1c6f4563df7 |
|---|---|
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
|
3 # $Id$ |
|
4 # |
2 # |
5 # polyml-platform --- determine Poly/ML's idea of current hardware and |
3 # polyml-platform --- determine Poly/ML's idea of current hardware and |
6 # operating system type |
4 # operating system type |
7 # |
5 # |
8 # NOTE: platform identifiers should be kept as generic as possible, |
6 # NOTE: platform identifiers should be kept as generic as possible, |