equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
|
3 # $Id$ |
|
4 # |
2 # |
5 # polyml-version --- determine Poly/ML runtime system version |
3 # polyml-version --- determine Poly/ML runtime system version |
6 |
4 |
7 echo -n polyml |
5 echo -n polyml |
8 |
6 |