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@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@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."