equal
deleted
inserted
replaced
1 #!/bin/sh |
1 #!/bin/sh |
2 |
2 |
3 CONFIGURE_EXECUTABLE="$_" |
3 CONFIGURE_EXECUTABLE="$_" |
4 # On *nix systems those two are equal when ./configure is done |
4 # On *nix systems those two are equal when ./configure is done |
5 if [ "$0" != "$CONFIGURE_EXECUTABLE" ]; then |
5 if [ "$0" != "$CONFIGURE_EXECUTABLE" ]; then |
6 if [ -z "`echo $CONFIGURE_EXECUTABLE | grep make`" ]; then |
6 # On some systems, when ./configure is triggered from 'make' |
|
7 # the $_ is filled with 'make'. So if that is true, skip 'make' |
|
8 # and use $0 (and hope that is correct ;)) |
|
9 if [ -n "`echo $CONFIGURE_EXECUTABLE | grep make`" ]; then |
7 CONFIGURE_EXECUTABLE="$0" |
10 CONFIGURE_EXECUTABLE="$0" |
8 else |
11 else |
9 CONFIGURE_EXECUTABLE="$CONFIGURE_EXECUTABLE $0" |
12 CONFIGURE_EXECUTABLE="$CONFIGURE_EXECUTABLE $0" |
10 fi |
13 fi |
11 fi |
14 fi |