coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Makefile: Revert r10015, which was based on a misunderstanding	lmamane	2007-07-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10022 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: needs GNU Make 3.81	lmamane	2007-07-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10020 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: more robustness all around	lmamane	2007-07-18
\| \| \| \| \| \| \| \|	- Make sure make notices when a command fails - don't leave behind half-baked output files of commands that failed git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10016 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: Do _not_ delete dummy .ml files of .ml4 files even when not needed ↵	lmamane	2007-07-17
\| \| \| \| \| \|	anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10015 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: -MG doesn't (and can't) do what is necessary	lmamane	2007-07-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	The -MG option causes gcc to add any non-found .h file verbatim in the dependencies. This naturally doesn't include the path to it (because the path is unknown) and thus make doesn't know how to build it; it knows how to build kernel/byterun/coq_jumptbl.h, not "coq_jumptbl.h". --This line, and those below, will be ignored-- M Makefile.common M Makefile.build git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10011 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A cleaner solution to "make deletes .ml4.d files -> infinite loop" problem	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10010 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oups... empty .ml4.d files produced	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10009 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CAMLP4DEPS will not work for .byteml and .optml	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10008 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Generalized CAMLP4USE for pp dependencies	corbinea	2007-07-16
\| \| \| \| \| \| \| \|	Removed parsing/lexer.ml4 special case No file depends on pa_extend_m.cmo anymore, Wierd ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10007 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: work around gcc bug: lhs of make rule created by -MM does not ↵	lmamane	2007-07-16
\| \| \| \| \| \|	include path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10006 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: in C, .d files need to depend on the same as the .o file	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10005 85f007b7-540e-0410-9357-904b9bb8a0f7
*	makefile: dependencies of .c files: assume missing headers are generated files	lmamane	2007-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10004 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Makefile: use CFLAGS for dependency generation of .c files	lmamane	2007-07-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10003 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A emacs-specific comment to use makefile-mode on Makefile.*	letouzey	2007-07-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9999 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New bootstrapping, improved, Makefile system	corbinea	2007-07-13
	Documented in dev/doc/build-system.txt . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9992 85f007b7-540e-0410-9357-904b9bb8a0f7