End of a nightmare: patch for GiNaC's acinclude.m4

[Roberto Bagnara]

A student of mine started having troubles with her Linux machine at
home soon after she started playing with GiNaC.  The machine seemed to
become instable after a few days of work and she reinstalled GNU/Linux
several times because of that.  A few days ago, we discovered that
/dev/null was no longer a character device: it was an ordinary file
and that caused the system not to boot properly.  We recreated the
/dev/null device and everything seemed to go well until this morning,
when the device disappeared again.  BUT this time Tatiana provided
the relevant bit of information; here it is:

    ...
    config.status: creating doc/reference/Makefile 
    config.status: creating config.h 
    **** The following problems have been detected by configure. 
    **** Please check the messages below before running "make". 
    **** (see the section 'Common Problems' in the INSTALL file) 
    
    ** No suitable installed version of CLN could be found. 
    
    deleting cache /dev/null 
    [root at crystal GiNaC-1.0.3]# 

Aaargh!!!  It was GiNaC configuration erasing /dev/null!
Yeah, right, there is no need to run `configure' while
being root.  However, I feel in this case the price that
had to be payed was a bit too high.  That is why I propose
the following patch is applied to `acinclude.m4':
if `cache_file' is `/dev/null' do not delete it.
All the best,

   Roberto

--
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it


diff -rcp GiNaC-1.0.3.orig/acinclude.m4 GiNaC-1.0.3/acinclude.m4
*** GiNaC-1.0.3.orig/acinclude.m4	Tue Nov 20 18:42:05 2001
--- GiNaC-1.0.3/acinclude.m4	Tue Jan 15 09:56:33 2002
*************** if test "x${ginac_error}" = "xyes"; then
*** 86,93 ****
      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."
--- 86,95 ----
      if test "x${ginac_warning_txt}" != "x"; then
          echo "${ginac_warning_txt}"
      fi
!     if test "x$cache_file" != "x/dev/null"
!         echo "deleting cache ${cache_file}"
!         rm -f $cache_file
!     fi
      else 
          if test x$ginac_warning = xyes; then
              echo "=== The following minor problems have been detected by configure."