+
+if test "x${ginac_error}" = "xyes"; then
+ 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"
+ fi
+ echo "Configuration of GiNaC $VERSION done. Now type \"make\"."
+fi