> don't worry about it, > doc/Makefile isn't called from the top-level Makefile, > it has to be run manually. There's no reason for the user > to run make in doc/ because we rerun texi and check in > all 3 files after any change. OK, perfect :) -- Jean Delvare http://www.ensicaen.ismra.fr/~delvare/
