2006-09-14 07:09:04 +02:00
|
|
|
#!/usr/bin/bash
|
2005-05-18 13:23:29 +02:00
|
|
|
path=`dirname $0`
|
2006-09-14 07:09:04 +02:00
|
|
|
. "$path/SETUP.sh"
|
|
|
|
extra_flags=""
|
|
|
|
extra_configs="$max_configs"
|
2000-12-18 22:24:19 +01:00
|
|
|
|
2006-09-14 07:09:04 +02:00
|
|
|
. "$path/FINISH.sh"
|