equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
|
2 |
|
3 set -x |
2 |
4 |
3 if [ -z "$1" ]; then |
5 if [ -z "$1" ]; then |
4 echo "Where config file?" |
6 echo "Where config file?" |
5 exit 1 |
7 exit 1 |
6 fi |
8 fi |
14 check_platform() { |
16 check_platform() { |
15 case `uname -s` in |
17 case `uname -s` in |
16 CYGWIN_NT-*) |
18 CYGWIN_NT-*) |
17 host_os=windows |
19 host_os=windows |
18 host_distro=cygwin |
20 host_distro=cygwin |
|
21 ;; |
|
22 MINGW64_NT-*) |
|
23 host_os=windows |
|
24 host_distro=mingw64 |
19 ;; |
25 ;; |
20 Linux) |
26 Linux) |
21 host_os=linux |
27 host_os=linux |
22 if [ -e /etc/debian_version ]; then |
28 if [ -e /etc/debian_version ]; then |
23 host_distro=debian |
29 host_distro=debian |