equal
deleted
inserted
replaced
23 if ! [ -f "config.cache" ]; then |
23 if ! [ -f "config.cache" ]; then |
24 echo "can't reconfigure, because never configured before" |
24 echo "can't reconfigure, because never configured before" |
25 exit 1 |
25 exit 1 |
26 fi |
26 fi |
27 # Make sure we don't lock config.cache |
27 # Make sure we don't lock config.cache |
28 configure=`cat config.cache` |
28 cat config.cache > cache.tmp |
29 $configure |
29 sh cache.tmp |
|
30 rm -f cache.tmp |
30 exit $? |
31 exit $? |
31 fi |
32 fi |
32 |
33 |
33 set_default |
34 set_default |
34 detect_params "$@" |
35 detect_params "$@" |