diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-08-11 14:55:38 +0200 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-08-11 14:55:38 +0200 |
| commit | 2d0357b3939dda9fa958c2c0ba97e366129df602 (patch) | |
| tree | f8111159d3b86a1ceda1158b4b54cac9380e8725 /reproduce/config/pipeline | |
| parent | ea44dfc50926fb7b5d7b67d1b632ef3eb780b579 (diff) | |
Shell to run configure script set to /bin/sh
We had previously started the `configure' script with `/bin/bash'. But this
script is meant to check for Bash inside of it. So to be run-able (on a
system which may not have Bash), the `configure' script has to be run by
`/bin/sh'.
Diffstat (limited to 'reproduce/config/pipeline')
0 files changed, 0 insertions, 0 deletions