- 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
+ 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