diff options
author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2020-01-23 19:17:16 +0000 |
---|---|---|
committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2020-01-23 19:21:15 +0000 |
commit | cccf8782014beb85b8c8cb23d6ece56c849773f3 (patch) | |
tree | a1347b7090f1333086f62c1f20655ebd3fb0a3e5 /project | |
parent | 2264c0fea5668cd8f827cdbd89004fd390b0b14f (diff) |
Hashbangs of project and configure.sh set to /bin/sh
Until now, the hashbang of these two shell scripts was set to `/bin/bash',
hence assuming that GNU Bash exists on the host system! But this is an
extra requirement on the host operating system and these two scripts should
be written such that they operate on a POSIX shell (the generic `/bin/sh'
which can point to any shell program).
With this commit this has been implemented! We may confront some errors as
the system is run on other systems, but we should fix such errors and work
hard to make these two scripts as POSIX-compatible as possible (runnable on
any shell, so as not to force users to install Bash before running the
project).
This completes Task #15525.
Diffstat (limited to 'project')
-rwxr-xr-x | project | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -1,4 +1,4 @@ -#!/bin/bash +#!/bin/sh # # High-level script to manage the project. # Run `./project --help' for a description of how to use it. |