equal
deleted
inserted
replaced
129 #killcmd=/bin/kill |
129 #killcmd=/bin/kill |
130 killcmd=kill |
130 killcmd=kill |
131 |
131 |
132 # This can be increased if timing seems to be an issue. |
132 # This can be increased if timing seems to be an issue. |
133 sleep_seconds=1 |
133 sleep_seconds=1 |
|
134 if [ -n "$TIMEOUT_FACTOR" ] ; then |
|
135 sleep_seconds=$(echo $TIMEOUT_FACTOR $sleep_seconds | awk '{printf "%d\n", int($1 * $2)}') |
|
136 fi |
134 |
137 |
135 echo "ShellScaffold.sh: Version" >& 2 |
138 echo "ShellScaffold.sh: Version" >& 2 |
136 topPid=$$ |
139 topPid=$$ |
137 |
140 |
138 # Be careful to echo to >& in these general functions. |
141 # Be careful to echo to >& in these general functions. |