Changeset 4371

Timestamp:

Oct 26, 2012, 11:52:50 AM (10 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.

Location:

trunk

Files:

• client/servlet/test/src/webservice/run.sh (modified) (1 diff)
• client/servlet/www/WEB-INF/init.sh (modified) (1 diff)
• client/servlet/www/WEB-INF/update.sh (modified) (1 diff)
• doc/course/install.sh (modified) (1 diff)
• doc/course/src/exercise/bin/new_project.sh (modified) (1 diff)
• misc/install/install.sh (modified) (1 diff)
• misc/shell.sh (modified) (1 diff)

trunk/client/servlet/test/src/webservice/run.sh

@@ -1 @@
-#!/bin/sh
+#!/bin/bash
 . ./config.sh
 

trunk/client/servlet/www/WEB-INF/init.sh

@@ -1 @@
-#!/bin/sh
+#!/bin/bash
 
 # $Id$

trunk/client/servlet/www/WEB-INF/update.sh

@@ -1 @@
-#!/bin/sh
+#!/bin/bash
 
 # $Id$

trunk/doc/course/install.sh

@@ -1 @@
-#!/bin/sh
+#!/bin/bash
 rsync -av build/ /srv/www/htdocs/
 

trunk/doc/course/src/exercise/bin/new_project.sh

@@ -1 @@
-#!/bin/sh
+#!/bin/bash
 #
 # This script creates a project and registers files for one given user

trunk/misc/install/install.sh

@@ -1 @@
-#!/bin/sh
+#!/bin/bash
 # $Id$
 

trunk/misc/shell.sh

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