aboutsummaryrefslogtreecommitdiff
path: root/project
diff options
context:
space:
mode:
authorMohammad Akhlaghi <mohammad@akhlaghi.org>2020-01-23 19:17:16 +0000
committerMohammad Akhlaghi <mohammad@akhlaghi.org>2020-01-23 19:21:15 +0000
commitcccf8782014beb85b8c8cb23d6ece56c849773f3 (patch)
treea1347b7090f1333086f62c1f20655ebd3fb0a3e5 /project
parent2264c0fea5668cd8f827cdbd89004fd390b0b14f (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-xproject2
1 files changed, 1 insertions, 1 deletions
diff --git a/project b/project
index d994b09..264895a 100755
--- a/project
+++ b/project
@@ -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.