diff options
| author | Maxime Dénès | 2017-07-20 13:14:38 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-07-20 13:14:38 +0200 |
| commit | 945d7bfa27b71137d86a4a46aeeced90d4b59303 (patch) | |
| tree | 438561788f99b0896eb905aeaf19b93e6687c3a5 /install.sh | |
| parent | 4d4ec6a095d01b6117ac3682d8a7882b1a2520e7 (diff) | |
| parent | d074e889b3cdfe8c292d3c52a4ed005789384fc0 (diff) | |
Merge branch 'v8.7'
Diffstat (limited to 'install.sh')
| -rwxr-xr-x | install.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/install.sh b/install.sh index c5835b0143..f8589a3c71 100755 --- a/install.sh +++ b/install.sh @@ -8,7 +8,7 @@ for f; do dn=`dirname $f` install -d "$dest/$dn" case $bn in - *.cmxs) install -m 755 $f "$dest/$dn/$bn" + *.cmxs|*.py) install -m 755 $f "$dest/$dn/$bn" ;; *) install -m 644 $f "$dest/$dn/$bn" ;; |