changeset 3770 | 12d0e59df0fb |
parent 10 | 06bc494ca11e |
child 3890 | b53fced26fa4 |
3769:5fd6cfd5a9a0 | 3770:12d0e59df0fb |
---|---|
41 fi |
41 fi |
42 |
42 |
43 # set platform-dependent variables |
43 # set platform-dependent variables |
44 OS=`uname -s` |
44 OS=`uname -s` |
45 case "$OS" in |
45 case "$OS" in |
46 SunOS | Linux ) |
46 SunOS | Linux | CYGWIN* ) |
47 NULL=/dev/null |
|
48 PS=":" |
47 PS=":" |
49 FS="/" |
48 FS="/" |
50 ;; |
49 ;; |
51 Windows* ) |
50 Windows* ) |
52 NULL=NUL |
|
53 PS=";" |
51 PS=";" |
54 FS="\\" |
52 FS="\\" |
55 ;; |
53 ;; |
56 * ) |
54 * ) |
57 echo "Unrecognized system!" |
55 echo "Unrecognized system!" |