Changeset 4371 for trunk/misc/shell.sh

Timestamp:

Oct 26, 2012, 11:52:50 AM (11 years ago)

Author:

olle

Message:

Refs #788. Unix/Linux *.sh shell scripts have the shebang line changed from "#!/bin/sh" to "#!/bin/bash", in order to make the scripts work on Ubunto Linux without explicitly defining the shell.

File:

• trunk/misc/shell.sh (modified) (1 diff)

trunk/misc/shell.sh

@@ -1 @@
-#!/bin/sh
+#!/bin/bash
 PS1="ProSE: "