- echo "**** The following 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_error_txt"
- if test "x${ginac_warning_txt}" != "x"; then
- echo "${ginac_warning_txt}"
- fi
- 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"
+ echo "**** The following 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_error_txt"
+ if test "x${ginac_warning_txt}" != "x"; then
+ echo "${ginac_warning_txt}"