- echo "deleting cache ${cache_file}"
- rm -f $cache_file
- else
- if test x$ginac_warning = xyes; then
- echo "=== The following minor problems have been detected by configure."
- echo "=== Please check the messages below before running \"make\"."
- echo "=== (see the section 'Common Problems' in the INSTALL file)"
- echo "$ginac_warning_txt"
- fi
+ if test "x$cache_file" != "x/dev/null"; then
+ echo "deleting cache ${cache_file}"
+ rm -f $cache_file
+ fi
+ exit 1
+else
+ if test "x${ginac_warning}" = "xyes"; then
+ echo "=== The following minor problems have been detected by configure."
+ echo "=== Please check the messages below before running \"make\"."
+ echo "=== (see the section 'Common Problems' in the INSTALL file)"
+ echo "$ginac_warning_txt"
+ fi